let G3, G4 be _Graph; :: thesis:
let v1, v2 be object ; :: thesis:
let G1 be addVertex of G3,v1; :: thesis:
let G2 be addVertex of G4,v2; :: thesis:
let F0 be PGraphMapping of G3,G4; :: thesis:
assume ( not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 ) ; :: thesis:
then consider F being PGraphMapping of G1,G2 such that
A1: F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] 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 ) and
( F0 is semi-continuous implies F is semi-continuous ) and
A6: ( F0 is continuous implies F is continuous ) and
( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) and
( F0 is Dcontinuous implies F is Dcontinuous ) by Th148;
take F ; :: thesis:
thus F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] by A1; :: thesis:
thus ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) by A2, A4; :: thesis:
thus ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) by A2, A4, A6; :: 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: