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,v4,e2,v2; :: thesis:
let F0 be PGraphMapping of G3,G4; :: thesis:
assume that
A1: ( 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 ) and
A2: ( v3 in dom (F0 _V) & (F0 _V) . v3 = v4 ) ; :: thesis:
consider G5 being addVertex of G3,v1 such that
A3: G1 is addEdge of G5,v1,e1,v3 by A1, GLIB_006:126;
consider G6 being addVertex of G4,v2 such that
A4: G2 is addEdge of G6,v4,e2,v2 by A1, GLIB_006:125;
consider F1 being PGraphMapping of G5,G6 such that
A5: F1 = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] and
A6: ( F0 is total implies F1 is total ) and
A7: ( F0 is onto implies F1 is onto ) and
A8: ( F0 is one-to-one implies F1 is one-to-one ) and
( F0 is directed implies F1 is directed ) and
( F0 is semi-continuous implies F1 is semi-continuous ) and
( F0 is continuous implies F1 is continuous ) and
( F0 is semi-Dcontinuous implies F1 is semi-Dcontinuous ) and
( F0 is Dcontinuous implies F1 is Dcontinuous ) by A1, Th148;
A9: ( v1 in dom (F1 _V) & v3 in dom (F1 _V) & (F1 _V) . v1 = v2 & (F1 _V) . v3 = v4 )

end;