let G3, G4 be _Graph; :: thesis:
let v3 be Vertex of G3; :: thesis:
let v4 be Vertex of G4; :: thesis:
let e1, e2, v1, v2 be object ; :: thesis:
let G1 be addAdjVertex of G3,v1,e1,v3; :: thesis:
let G2 be addAdjVertex of G4,v2,e2,v4; :: thesis:
let F0 be PGraphMapping of G3,G4; :: thesis:
assume ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 ) ; :: thesis:
then consider F being PGraphMapping of G1,G2 such that
A1: F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] and
A2: ( F0 is total implies F is total ) and
A3: ( F0 is onto implies F is onto ) and
A4: ( F0 is one-to-one implies F is one-to-one ) and
A5: ( F0 is directed implies F is directed ) by Th155;
take F ; :: thesis:
thus F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] by A1; :: thesis:
thus ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) by A2, A4; :: thesis:
thus ( F0 is isomorphism implies F is isomorphism ) by A2, A3, A4; :: thesis:
thus ( F0 is Disomorphism implies F is Disomorphism ) by A2, A3, A4, A5; :: thesis: