let G3, G4 be _Graph; :: thesis:
let V1, V2 be set ; :: thesis:
let G1 be addLoops of G3,V1; :: thesis:
let G2 be addLoops of G4,V2; :: thesis:
let F0 be PGraphMapping of G3,G4; :: thesis:
assume that
A1: ( V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 ) and
A2: ( (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 ) ; :: thesis:
( the_Vertices_of G1 = the_Vertices_of G3 & the_Vertices_of G2 = the_Vertices_of G4 ) by A1, Def5;
then reconsider f = F0 _V as PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) ;
consider E1 being set , f1 being one-to-one Function such that
A3: ( E1 misses the_Edges_of G3 & the_Edges_of G1 = (the_Edges_of G3) \/ E1 & dom f1 = E1 & rng f1 = V1 & the_Source_of G1 = (the_Source_of G3) +* f1 & the_Target_of G1 = (the_Target_of G3) +* f1 ) by A1, Def5;
consider E2 being set , f2 being one-to-one Function such that
A4: ( E2 misses the_Edges_of G4 & the_Edges_of G2 = (the_Edges_of G4) \/ E2 & dom f2 = E2 & rng f2 = V2 & the_Source_of G2 = (the_Source_of G4) +* f2 & the_Target_of G2 = (the_Target_of G4) +* f2 ) by A2, Def5;
set h = ((f2 ") * ((F0 _V) | V1)) * f1;
set g = (F0 _E) +* (((f2 ") * ((F0 _V) | V1)) * f1);
A5: dom ((F0 _E) +* (((f2 ") * ((F0 _V) | V1)) * f1)) = (dom (F0 _E)) \/ (dom (((f2 ") * ((F0 _V) | V1)) * f1)) by FUNCT_4:def 1;
A6: dom (f2 ") = rng ((F0 _V) | V1) by A2, A4, FUNCT_1:33;
then A7: dom ((f2 ") * ((F0 _V) | V1)) = rng f1 by A2, A3, RELAT_1:27;
then A8: dom (((f2 ") * ((F0 _V) | V1)) * f1) = E1 by A3, RELAT_1:27;
then A9: dom ((F0 _E) +* (((f2 ") * ((F0 _V) | V1)) * f1)) c= the_Edges_of G1 by A3, A5, XBOOLE_1:9;
rng ((f2 ") * ((F0 _V) | V1)) = rng (f2 ") by A6, RELAT_1:28
.= E2 by A4, FUNCT_1:33 ;
then A10: rng (((f2 ") * ((F0 _V) | V1)) * f1) = E2 by A7, RELAT_1:28;
A11: rng ((F0 _E) +* (((f2 ") * ((F0 _V) | V1)) * f1)) c= (rng (F0 _E)) \/ (rng (((f2 ") * ((F0 _V) | V1)) * f1)) by FUNCT_4:17;
(rng (F0 _E)) \/ (rng (((f2 ") * ((F0 _V) | V1)) * f1)) c= (the_Edges_of G4) \/ E2 by A10, XBOOLE_1:9;
then rng ((F0 _E) +* (((f2 ") * ((F0 _V) | V1)) * f1)) c= the_Edges_of G2 by A4, A11, XBOOLE_1:1;
then reconsider g = (F0 _E) +* (((f2 ") * ((F0 _V) | V1)) * f1) as PartFunc of (the_Edges_of G1),(the_Edges_of G2) by A9, RELSET_1:4;
A12: dom (((F0 _V) | V1) * f1) = dom f1 by A2, A3, RELAT_1:27;

now :: thesis:

hereby :: thesis:

let e be object ; :: thesis:
set v = (the_Source_of G1) . e;
set w = (the_Target_of G1) . e;
assume e in dom g ; :: thesis:

per cases by FUNCT_4:12;

suppose A13: e in dom (F0 _E) ; :: thesis:

then ( (the_Source_of G1) . e = (the_Source_of G3) . e & (the_Target_of G1) . e = (the_Target_of G3) . e ) by GLIB_006:def 9;
hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A13, GLIB_010:5; :: thesis:

end;

suppose e in dom (((f2 ") * ((F0 _V) | V1)) * f1) ; :: thesis:

then A14: e in dom f1 by A3, A8;
then ( (the_Source_of G1) . e = f1 . e & (the_Target_of G1) . e = f1 . e ) by A3, FUNCT_4:13;
then ( (the_Source_of G1) . e in V1 & (the_Target_of G1) . e in V1 ) by A3, A14, FUNCT_1:3;
hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A2, RELAT_1:57; :: thesis:

end;

let e, v, w be object ; :: thesis:
assume A15: ( e in dom g & v in dom f & w in dom f ) ; :: thesis:
assume A16: e Joins v,w,G1 ; :: thesis:

per cases by A15, FUNCT_4:12;

suppose A17: e in dom (F0 _E) ; :: thesis:

then e Joins v,w,G3 by A16, GLIB_006:72;
then A18: (F0 _E) . e Joins (F0 _V) . v,(F0 _V) . w,G4 by A15, A17, GLIB_010:4;
not e in E1 by A3, A15, A17, XBOOLE_0:5;
then g . e Joins f . v,f . w,G4 by A8, A18, FUNCT_4:11;
hence g . e Joins f . v,f . w,G2 by GLIB_006:70; :: thesis:

end;

suppose e in dom (((f2 ") * ((F0 _V) | V1)) * f1) ; :: thesis:

then A19: ( e in E1 & g . e = (((f2 ") * ((F0 _V) | V1)) * f1) . e ) by A8, FUNCT_4:13;
then ( (the_Source_of G1) . e = f1 . e & (the_Target_of G1) . e = f1 . e ) by A3, FUNCT_4:13;
then A20: ( v = f1 . e & w = f1 . e ) by A16, GLIB_000:def 13;
then A21: v in V1 by A3, A19, FUNCT_1:3;
then A22: f . v = ((F0 _V) | V1) . v by FUNCT_1:49;
then A23: f . v in V2 by A2, A21, FUNCT_1:3;
then f . v in dom (f2 ") by A4, FUNCT_1:33;
then (f2 ") . (f . v) in rng (f2 ") by FUNCT_1:3;
then A24: (f2 ") . (f . v) in dom f2 by FUNCT_1:33;
then ( (the_Source_of G2) . ((f2 ") . (f . v)) = f2 . ((f2 ") . (f . v)) & (the_Target_of G2) . ((f2 ") . (f . v)) = f2 . ((f2 ") . (f . v)) ) by A4, FUNCT_4:13;
then A25: ( (the_Source_of G2) . ((f2 ") . (f . v)) = f . v & (the_Target_of G2) . ((f2 ") . (f . v)) = f . v ) by A4, A23, FUNCT_1:35;
(f2 ") . (f . v) in the_Edges_of G2 by A4, A24, XBOOLE_0:def 3;
then (f2 ") . (((F0 _V) | V1) . v) Joins f . v,f . v,G2 by A22, A25, GLIB_000:def 13;
then (f2 ") . ((((F0 _V) | V1) * f1) . e) Joins f . v,f . w,G2 by A3, A19, A20, FUNCT_1:13;
then ((f2 ") * (((F0 _V) | V1) * f1)) . e Joins f . v,f . w,G2 by A3, A12, A19, FUNCT_1:13;
hence g . e Joins f . v,f . w,G2 by A19, RELAT_1:36; :: thesis:

end;

then reconsider F = [f,g] as PGraphMapping of G1,G2 by GLIB_010:8;
take F ; :: thesis:
thus F _V = F0 _V ; :: thesis:
A26: dom (F0 _E) misses dom (((f2 ") * ((F0 _V) | V1)) * f1) by A3, A8, XBOOLE_1:63;
hence (F _E) | (dom (F0 _E)) = F0 _E by FUNCT_4:33; :: thesis:

hereby :: thesis:

assume not F0 is empty ; :: thesis:
then dom (F _V) <> {} ;
hence not F is empty ; :: thesis:

end;

thus A27: ( F0 is total implies F is total ) :: thesis:

proof

assume F0 is total ; :: thesis:
then A28: ( dom (F0 _V) = the_Vertices_of G3 & dom (F0 _E) = the_Edges_of G3 ) by GLIB_010:def 11;
then A29: dom (F _V) = the_Vertices_of G1 by A1, Def5;
dom (F _E) = the_Edges_of G1 by A3, A8, A28, FUNCT_4:def 1;
hence F is total by A29, GLIB_010:def 11; :: thesis:

end;

thus A30: ( F0 is onto implies F is onto ) :: thesis:

proof

assume F0 is onto ; :: thesis:
then A31: ( rng (F0 _V) = the_Vertices_of G4 & rng (F0 _E) = the_Edges_of G4 ) by GLIB_010:def 12;
then A32: rng (F _V) = the_Vertices_of G2 by A2, Def5;
rng (F _E) = the_Edges_of G2 by A4, A10, A26, A31, NECKLACE:6;
hence F is onto by A32, GLIB_010:def 12; :: thesis:

end;

thus A33: ( F0 is one-to-one implies F is one-to-one ) :: thesis:

proof

assume A34: F0 is one-to-one ; :: thesis:
rng (F0 _E) misses E2 by A4, XBOOLE_1:63;
then ( F _V is one-to-one & F _E is one-to-one ) by A2, A10, A34, FUNCT_4:92;
hence F is one-to-one by GLIB_010:def 13; :: thesis:

end;

thus A35: ( F0 is directed implies F is directed ) :: thesis:

proof

assume A36: F0 is directed ; :: thesis:

now :: thesis:

let e, v, w be object ; :: thesis:
assume A37: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis:
assume A38: e DJoins v,w,G1 ; :: thesis:

per cases by A37, FUNCT_4:12;

suppose A39: e in dom (F0 _E) ; :: thesis:

then e DJoins v,w,G3 by A38, GLIB_006:71;
then A40: (F0 _E) . e DJoins (F0 _V) . v,(F0 _V) . w,G4 by A36, A37, A39, GLIB_010:def 14;
not e in E1 by A3, A37, A39, XBOOLE_0:5;
then g . e DJoins f . v,f . w,G4 by A8, A40, FUNCT_4:11;
hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by GLIB_006:70; :: thesis:

end;

suppose e in dom (((f2 ") * ((F0 _V) | V1)) * f1) ; :: thesis:

then A41: ( e in E1 & g . e = (((f2 ") * ((F0 _V) | V1)) * f1) . e ) by A8, FUNCT_4:13;
then ( (the_Source_of G1) . e = f1 . e & (the_Target_of G1) . e = f1 . e ) by A3, FUNCT_4:13;
then A42: ( v = f1 . e & w = f1 . e ) by A38, GLIB_000:def 14;
then A43: v in V1 by A3, A41, FUNCT_1:3;
then A44: f . v = ((F0 _V) | V1) . v by FUNCT_1:49;
then A45: f . v in V2 by A2, A43, FUNCT_1:3;
then f . v in dom (f2 ") by A4, FUNCT_1:33;
then (f2 ") . (f . v) in rng (f2 ") by FUNCT_1:3;
then A46: (f2 ") . (f . v) in dom f2 by FUNCT_1:33;
then ( (the_Source_of G2) . ((f2 ") . (f . v)) = f2 . ((f2 ") . (f . v)) & (the_Target_of G2) . ((f2 ") . (f . v)) = f2 . ((f2 ") . (f . v)) ) by A4, FUNCT_4:13;
then A47: ( (the_Source_of G2) . ((f2 ") . (f . v)) = f . v & (the_Target_of G2) . ((f2 ") . (f . v)) = f . v ) by A4, A45, FUNCT_1:35;
(f2 ") . (f . v) in the_Edges_of G2 by A4, A46, XBOOLE_0:def 3;
then (f2 ") . (((F0 _V) | V1) . v) DJoins f . v,f . v,G2 by A44, A47, GLIB_000:def 14;
then (f2 ") . ((((F0 _V) | V1) * f1) . e) DJoins f . v,f . w,G2 by A3, A41, A42, FUNCT_1:13;
then ((f2 ") * (((F0 _V) | V1) * f1)) . e DJoins f . v,f . w,G2 by A3, A12, A41, FUNCT_1:13;
hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A41, RELAT_1:36; :: thesis:

end;

hence F is directed by GLIB_010:def 14; :: thesis:

end;

thus ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) by A27, A33; :: thesis:
thus ( F0 is isomorphism implies F is isomorphism ) by A27, A30, A33; :: thesis:
thus ( F0 is Disomorphism implies F is Disomorphism ) by A27, A30, A33, A35; :: thesis: