let V, A be set ; for a, b being Element of V
for x, y being object
for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds
<*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_main_part (V,A,a,b,x,y)),(PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))*> is SFHT of (ND (V,A))
let a, b be Element of V; for x, y being object
for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds
<*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_main_part (V,A,a,b,x,y)),(PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))*> is SFHT of (ND (V,A))
let x, y be object ; for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds
<*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_main_part (V,A,a,b,x,y)),(PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))*> is SFHT of (ND (V,A))
let x0, y0 be Nat; ( not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) implies <*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_main_part (V,A,a,b,x,y)),(PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))*> is SFHT of (ND (V,A)) )
assume A1:
( not V is empty & A is_without_nonatomicND_wrt V & a <> b & a <> y & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) )
; <*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_main_part (V,A,a,b,x,y)),(PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))*> is SFHT of (ND (V,A))
set f = gcd_var_init (V,A,a,b,x,y);
set g = gcd_main_loop (V,A,a,b);
set p = valid_gcd_input (V,A,x,y,x0,y0);
set q = gcd_inv (V,A,a,b,x0,y0);
set r = PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)));
A2:
<*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_var_init (V,A,a,b,x,y)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
by A1, Th16;
A3:
<*(gcd_inv (V,A,a,b,x0,y0)),(gcd_main_loop (V,A,a,b)),(PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))*> is SFHT of (ND (V,A))
by A1, Th23;
<*(PP_inversion (gcd_inv (V,A,a,b,x0,y0))),(gcd_main_loop (V,A,a,b)),(PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))*> is SFHT of (ND (V,A))
by NOMIN_3:19;
hence
<*(valid_gcd_input (V,A,x,y,x0,y0)),(gcd_main_part (V,A,a,b,x,y)),(PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))*> is SFHT of (ND (V,A))
by A2, A3, NOMIN_3:25; verum