Fixed function cont_pos. Previous definition of size F in main theorem...

Fixed function cont_pos. Previous definition of size F in main theorem excahnged by an exact value. Proofed Lemma size_of_Fn. Defined Lemma G_in_dnf and made first steps of proofing it.