let V, A be set ; :: thesis: for a, b being Element of V
for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & 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
<*(gcd_inv (V,A,a,b,x0,y0)),(gcd_conditional_step (V,A,a,b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
let a, b be Element of V; :: thesis: for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & 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
<*(gcd_inv (V,A,a,b,x0,y0)),(gcd_conditional_step (V,A,a,b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
let x0, y0 be Nat; :: thesis: ( not V is empty & A is_without_nonatomicND_wrt V & a <> b & 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 <*(gcd_inv (V,A,a,b,x0,y0)),(gcd_conditional_step (V,A,a,b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) )
assume that
A1: not V is empty and
A2: A is_without_nonatomicND_wrt V and
A3: a <> b and
A4: A is complex-containing and
A5: ( ( 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 ) ) ; :: thesis: <*(gcd_inv (V,A,a,b,x0,y0)),(gcd_conditional_step (V,A,a,b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
set i = gcd_inv (V,A,a,b,x0,y0);
set l = less (A,b,a);
A6: <*(PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))),(SC_assignment ((subtraction (A,a,b)),a)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) by A1, A2, A3, A4, A5, Th17;
<*(gcd_inv (V,A,a,b,x0,y0)),(PPid (ND (V,A))),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) by NOMIN_3:17;
then <*(PP_and ((PP_not (less (A,b,a))),(gcd_inv (V,A,a,b,x0,y0)))),(PPid (ND (V,A))),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) by NOMIN_3:4, NOMIN_3:15;
hence <*(gcd_inv (V,A,a,b,x0,y0)),(gcd_conditional_step (V,A,a,b)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) by A6, NOMIN_3:21; :: thesis: verum