let G3, G4 be _Graph; :: thesis: for V being set
for G1 being addLoops of G3,V
for G2 being addLoops of G4,V st G3 == G4 holds
G2 is G1 -Disomorphic
let V be set ; :: thesis: for G1 being addLoops of G3,V
for G2 being addLoops of G4,V st G3 == G4 holds
G2 is G1 -Disomorphic
let G1 be addLoops of G3,V; :: thesis: for G2 being addLoops of G4,V st G3 == G4 holds
G2 is G1 -Disomorphic
let G2 be addLoops of G4,V; :: thesis: ( G3 == G4 implies G2 is G1 -Disomorphic )
assume A1: G3 == G4 ; :: thesis: G2 is G1 -Disomorphic

per cases ( V c= the_Vertices_of G3 or not V c= the_Vertices_of G3 ) ;

suppose A2: V c= the_Vertices_of G3 ; :: thesis: G2 is G1 -Disomorphic

consider F0 being PGraphMapping of G3,G4 such that
A3: ( F0 = id G3 & F0 is Disomorphism ) by A1, GLIBPRE0:75;
A4: (F0 _V) | V is one-to-one by A3, FUNCT_1:52;
A5: dom ((F0 _V) | V) = (dom (F0 _V)) /\ V by RELAT_1:61
.= V by A2, A3, XBOOLE_1:28 ;
A6: rng ((F0 _V) | V) = ((id G3) _V) .: V by A3, RELAT_1:115
.= V by A2, FUNCT_1:92 ;
consider F being PGraphMapping of G1,G2 such that
( F _V = F0 _V & (F _E) | (dom (F0 _E)) = F0 _E ) and
( not F0 is empty implies not F is empty ) and
( F0 is total implies F is total ) and
( F0 is onto implies F is onto ) and
( F0 is one-to-one implies F is one-to-one ) and
( F0 is directed implies F is directed ) and
( F0 is weak_SG-embedding implies F is weak_SG-embedding ) and
( F0 is isomorphism implies F is isomorphism ) and
A7: ( F0 is Disomorphism implies F is Disomorphism ) by A2, A4, A5, A6, Th29;
thus G2 is G1 -Disomorphic by A3, A7, GLIB_010:def 24; :: thesis: verum

end;

suppose not V c= the_Vertices_of G3 ; :: thesis: G2 is G1 -Disomorphic

then ( G1 == G3 & not V c= the_Vertices_of G4 ) by A1, Def5, GLIB_000:def 34;
then ( G1 == G4 & G2 == G4 ) by A1, Def5, GLIB_000:85;
hence G2 is G1 -Disomorphic by GLIB_000:85, GLIBPRE0:76; :: thesis: verum

end;

end;