let V, A be set ; :: thesis: 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))
let a, b, z be Element of V; :: thesis: 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))
let x0, y0 be Nat; :: thesis: ( 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 <*(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)) )
set Da = denaming (V,A,a);
set Db = denaming (V,A,b);
set Dz = denaming (V,A,z);
set e = Equality (A,a,b);
set i = gcd_inv (V,A,a,b,x0,y0);
set q = PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)));
set r = valid_gcd_output (V,A,z,x0,y0);
set g = SC_assignment ((denaming (V,A,a)),z);
set P = PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))));
assume that
A2: A is complex-containing and
A3: for d being TypeSCNominativeData of V,A holds a is_complex_on d and
A4: for d being TypeSCNominativeData of V,A holds b is_complex_on d ; :: thesis: <*(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))
A5: for d being TypeSCNominativeData of V,A holds a is_a_value_on d by A2, A3, Th7;
A6: for d being TypeSCNominativeData of V,A holds b is_a_value_on d by A2, A4, Th7;
A9: dom (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom (Equality (A,a,b)) & (Equality (A,a,b)) . d = FALSE ) or ( d in dom (gcd_inv (V,A,a,b,x0,y0)) & (gcd_inv (V,A,a,b,x0,y0)) . d = FALSE ) or ( d in dom (Equality (A,a,b)) & (Equality (A,a,b)) . d = TRUE & d in dom (gcd_inv (V,A,a,b,x0,y0)) & (gcd_inv (V,A,a,b,x0,y0)) . d = TRUE ) ) } by NOMIN_2:17;
A10: dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b))) by A5, A6, Th11;
A11: dom (Equality (A,a,b)) c= dom (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) by PARTPR_2:3;
for d being TypeSCNominativeData of V,A st d in dom (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) & (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) . d = TRUE & d in dom (SC_assignment ((denaming (V,A,a)),z)) & (SC_assignment ((denaming (V,A,a)),z)) . d in dom (valid_gcd_output (V,A,z,x0,y0)) holds
(valid_gcd_output (V,A,z,x0,y0)) . ((SC_assignment ((denaming (V,A,a)),z)) . d) = TRUE

proof

let d be TypeSCNominativeData of V,A; :: thesis: ( d in dom (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) & (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) . d = TRUE & d in dom (SC_assignment ((denaming (V,A,a)),z)) & (SC_assignment ((denaming (V,A,a)),z)) . d in dom (valid_gcd_output (V,A,z,x0,y0)) implies (valid_gcd_output (V,A,z,x0,y0)) . ((SC_assignment ((denaming (V,A,a)),z)) . d) = TRUE )
assume that
A12: d in dom (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) and
(PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) . d = TRUE and
A13: d in dom (SC_assignment ((denaming (V,A,a)),z)) and
(SC_assignment ((denaming (V,A,a)),z)) . d in dom (valid_gcd_output (V,A,z,x0,y0)) ; :: thesis: (valid_gcd_output (V,A,z,x0,y0)) . ((SC_assignment ((denaming (V,A,a)),z)) . d) = TRUE
dom (PP_inversion (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))))) = { d where d is Element of ND (V,A) : not d in dom (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) } by PARTPR_2:def 17;
then consider d1 being Element of ND (V,A) such that
A14: d = d1 and
A15: not d1 in dom (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) by A12;
A16: dom (SC_assignment ((denaming (V,A,a)),z)) = dom (denaming (V,A,a)) by NOMIN_2:def 7;
not d1 in dom (Equality (A,a,b)) by A11, A15;
then A17: not d1 in dom (denaming (V,A,b)) by A10, A13, A14, A16, XBOOLE_0:def 4;
A18: dom (denaming (V,A,b)) = { d where d is NonatomicND of V,A : b in dom d } by NOMIN_1:def 18;
dom (gcd_inv (V,A,a,b,x0,y0)) = ND (V,A) by Def28;
then A19: d in dom (gcd_inv (V,A,a,b,x0,y0)) ;
( not d in dom (gcd_inv (V,A,a,b,x0,y0)) or (gcd_inv (V,A,a,b,x0,y0)) . d <> FALSE ) by A9, A14, A15;
then gcd_inv_pred V,A,a,b,x0,y0,d by A19, Def28;
hence (valid_gcd_output (V,A,z,x0,y0)) . ((SC_assignment ((denaming (V,A,a)),z)) . d) = TRUE by A14, A17, A18; :: thesis: verum

end;

hence <*(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)) by NOMIN_3:28; :: thesis: verum