theorem Th26: :: NOMIN_4:27

for V, A being set
for a, b, z being Element of V
for x0, y0 being Nat st 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
<*(PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))),(SC_assignment ((denaming (V,A,a)),z)),(valid_gcd_output (V,A,z,x0,y0))*> is SFHT of (ND (V,A))