let V, A be set ; :: thesis:
let a, b, z be Element of V; :: thesis:
let x0, y0 be Nat; :: thesis:
assume that
A1: not V is empty and
A2: A is_without_nonatomicND_wrt V and
A3: ( ( for d being TypeSCNominativeData of V,A holds a is_a_value_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_a_value_on d ) ) ; :: thesis:
set Da = denaming (V,A,a);
set Db = denaming (V,A,b);
set Dz = denaming (V,A,z);
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 E = Equality A;
set sp = SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z);
A4: <*(SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)),(SC_assignment ((denaming (V,A,a)),z)),(valid_gcd_output (V,A,z,x0,y0))*> is SFHT of (ND (V,A)) by NOMIN_3:29;
PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0))) ||= SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)

let d be Element of ND (V,A); :: according to NOMIN_3:def 3 :: thesis:
assume A5: ( d in dom (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) & (PP_and ((Equality (A,a,b)),(gcd_inv (V,A,a,b,x0,y0)))) . d = TRUE ) ; :: thesis:
reconsider dd = d as TypeSCNominativeData of V,A by NOMIN_1:39;
set X = { 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 ) ) } ;
d in { 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 A5, NOMIN_2:17;
then A6: ex d1 being TypeSCNominativeData of V,A st
( d = d1 & ( ( d1 in dom (Equality (A,a,b)) & (Equality (A,a,b)) . d1 = FALSE ) or ( d1 in dom (gcd_inv (V,A,a,b,x0,y0)) & (gcd_inv (V,A,a,b,x0,y0)) . d1 = FALSE ) or ( d1 in dom (Equality (A,a,b)) & (Equality (A,a,b)) . d1 = TRUE & d1 in dom (gcd_inv (V,A,a,b,x0,y0)) & (gcd_inv (V,A,a,b,x0,y0)) . d1 = TRUE ) ) ) ;
A7: dom (denaming (V,A,a)) = { d where d is NonatomicND of V,A : a in dom d } by NOMIN_1:def 18;
A8: d in dom (denaming (V,A,a))

dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b))) by Th11, A3;
hence d in dom (denaming (V,A,a)) by A5, A6, PARTPR_1:19, XBOOLE_0:def 4; :: thesis:

end;

consider D being NonatomicND of V,A such that
A9: d = D and
a in dom D by A8, A7;
A10: dom (valid_gcd_output (V,A,z,x0,y0)) = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } by Def26;
A11: (denaming (V,A,a)) . d is TypeSCNominativeData of V,A

proof

(denaming (V,A,a)) . d in ND (V,A) by PARTFUN1:4, A8;
then ex d1 being TypeSCNominativeData of V,A st (denaming (V,A,a)) . d = d1 ;
hence (denaming (V,A,a)) . d is TypeSCNominativeData of V,A ; :: thesis:

end;

A12: local_overlapping (V,A,d,((denaming (V,A,a)) . d),z) in dom (denaming (V,A,z))

proof

ex d2 being NonatomicND of V,A st
( d2 = d & a in dom d2 ) by A8, A7;
hence local_overlapping (V,A,d,((denaming (V,A,a)) . d),z) in dom (denaming (V,A,z)) by A1, A2, Th6, A11; :: thesis:

end;

then A13: local_overlapping (V,A,d,((denaming (V,A,a)) . d),z) in dom (valid_gcd_output (V,A,z,x0,y0)) by A10;
thus A14: d in dom (SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) :: thesis:

proof

dd in { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,a)) . d),z) in dom (valid_gcd_output (V,A,z,x0,y0)) & d in dom (denaming (V,A,a)) ) } by A8, A13;
hence d in dom (SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) by NOMIN_2:def 11; :: thesis:

end;

thus (SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) . d = TRUE :: thesis:

proof

set dlo = local_overlapping (V,A,D,((denaming (V,A,a)) . d),z);
A15: ( (SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) . dd = (valid_gcd_output (V,A,z,x0,y0)) . (local_overlapping (V,A,D,((denaming (V,A,a)) . d),z)) & dd in dom (denaming (V,A,a)) ) by A9, A14, NOMIN_2:35;
valid_gcd_output_pred V,A,z,x0,y0, local_overlapping (V,A,D,((denaming (V,A,a)) . d),z)

proof

gcd_inv_pred V,A,a,b,x0,y0,d by A5, A6, PARTPR_1:19, Def28;
then consider d2 being NonatomicND of V,A such that
A16: ( d = d2 & a in dom d2 & b in dom d2 & ex x, y being Nat st
( x = d2 . a & y = d2 . b & x gcd y = x0 gcd y0 ) ) ;
consider X, Y being Nat such that
A17: ( X = d2 . a & Y = d2 . b & X gcd Y = x0 gcd y0 ) by A16;
A18: (denaming (V,A,a)) . d in A

proof

a is_a_value_on dd by A3;
hence (denaming (V,A,a)) . d in A ; :: thesis:

end;

A19: d in dom (denaming (V,A,b))

proof

dom (Equality (A,a,b)) = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b))) by Th11, A3;
hence d in dom (denaming (V,A,b)) by A5, A6, PARTPR_1:19, XBOOLE_0:def 4; :: thesis:

end;

A20: (denaming (V,A,b)) . d in A

proof

b is_a_value_on dd by A3;
hence (denaming (V,A,b)) . d in A ; :: thesis:

end;

dom <:(denaming (V,A,a)),(denaming (V,A,b)):> = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b))) by FUNCT_3:def 7;
then A21: d in dom <:(denaming (V,A,a)),(denaming (V,A,b)):> by XBOOLE_0:def 4, A8, A19;
A22: (denaming (V,A,a)) . d = denaming (a,d2) by A8, A16, NOMIN_1:def 18
.= d2 . a by A16, NOMIN_1:def 12 ;
A23: (denaming (V,A,b)) . d = denaming (b,d2) by A19, A16, NOMIN_1:def 18
.= d2 . b by A16, NOMIN_1:def 12 ;
TRUE = (Equality A) . (<:(denaming (V,A,a)),(denaming (V,A,b)):> . d) by A5, A6, A21, FUNCT_1:13, PARTPR_1:19
.= (Equality A) . (((denaming (V,A,a)) . d),((denaming (V,A,b)) . d)) by FUNCT_3:def 7, A21 ;
then A24: (denaming (V,A,a)) . d = (denaming (V,A,b)) . d by A18, A20, Def9;
A25: X gcd Y = |.X.| by A24, A22, A23, A17, NEWTON02:3;
reconsider d1 = local_overlapping (V,A,D,((denaming (V,A,a)) . d),z) as NonatomicND of V,A by NOMIN_2:9;
A26: z in dom d1

proof

d1 in { d where d is NonatomicND of V,A : z in dom d } by A9, A12, NOMIN_1:def 18;
then ex dd1 being NonatomicND of V,A st
( d1 = dd1 & z in dom dd1 ) ;
hence z in dom d1 ; :: thesis:

end;

d1 . z = x0 gcd y0 by A1, A11, A22, A17, A25, NOMIN_2:10;
hence valid_gcd_output_pred V,A,z,x0,y0, local_overlapping (V,A,D,((denaming (V,A,a)) . d),z) by A26; :: thesis:

end;

hence (SC_Psuperpos ((valid_gcd_output (V,A,z,x0,y0)),(denaming (V,A,a)),z)) . d = TRUE by A15, A9, Def26, A13; :: thesis:

end;

hence <*(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 A4, NOMIN_3:15; :: thesis: