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

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