let G3 be _Graph; :: thesis: for G4 being G3 -Disomorphic _Graph
for V1, V2 being set
for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2 st card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) holds
G2 is G1 -Disomorphic
let G4 be G3 -Disomorphic _Graph; :: thesis: for V1, V2 being set
for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2 st card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) holds
G2 is G1 -Disomorphic
let V1, V2 be set ; :: thesis: for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2 st card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) holds
G2 is G1 -Disomorphic
let G1 be addVertices of G3,V1; :: thesis: for G2 being addVertices of G4,V2 st card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) holds
G2 is G1 -Disomorphic
let G2 be addVertices of G4,V2; :: thesis: ( card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) implies G2 is G1 -Disomorphic )
assume card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) ; :: thesis: G2 is G1 -Disomorphic
then consider f being Function such that
A1: ( f is one-to-one & dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) ) by CARD_1:5, WELLORD2:def 4;
reconsider f = f as one-to-one Function by A1;
consider F0 being PGraphMapping of G3,G4 such that
A2: F0 is Disomorphism by Def24;
consider F being PGraphMapping of G1,G2 such that
F = [((F0 _V) +* f),(F0 _E)] and
( F0 is weak_SG-embedding implies F is weak_SG-embedding ) and
( F0 is strong_SG-embedding implies F is strong_SG-embedding ) and
( F0 is isomorphism implies F is isomorphism ) and
A3: ( F0 is Disomorphism implies F is Disomorphism ) by A1, Th145;
thus G2 is G1 -Disomorphic by A2, A3; :: thesis: verum