let G3 be _Graph; for G4 being G3 -isomorphic _Graph
for G1 being addLoops of G3
for G2 being addLoops of G4 holds G2 is G1 -isomorphic
let G4 be G3 -isomorphic _Graph; for G1 being addLoops of G3
for G2 being addLoops of G4 holds G2 is G1 -isomorphic
let G1 be addLoops of G3; for G2 being addLoops of G4 holds G2 is G1 -isomorphic
let G2 be addLoops of G4; G2 is G1 -isomorphic
consider F0 being PGraphMapping of G3,G4 such that
A1:
F0 is isomorphism
by GLIB_010:def 23;
A2:
dom ((F0 _V) | (the_Vertices_of G3)) = the_Vertices_of G3
by A1, GLIB_010:def 11;
rng ((F0 _V) | (the_Vertices_of G3)) = the_Vertices_of G4
by A1, GLIB_010:def 12;
then 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
A3:
( F0 is isomorphism implies F is isomorphism )
and
( F0 is Disomorphism implies F is Disomorphism )
by A1, A2, Th29;
thus
G2 is G1 -isomorphic
by A1, A3, GLIB_010:def 23; verum