let G3, G4 be _Graph; :: thesis: for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let v3 be Vertex of G3; :: thesis: for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let v4 be Vertex of G4; :: thesis: for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let e1, e2, v1, v2 be object ; :: thesis: for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let G1 be addAdjVertex of G3,v3,e1,v1; :: thesis: for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let G2 be addAdjVertex of G4,v4,e2,v2; :: thesis: for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let F0 be PGraphMapping of G3,G4; :: thesis: ( 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 implies ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) ) )

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: ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

consider G5 being addVertex of G3,v1 such that

A3: G1 is addEdge of G5,v3,e1,v1 by A1, GLIB_006:125;

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

A9: ( 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;

A10: ( v1 in dom (F1 _V) & v3 in dom (F1 _V) & (F1 _V) . v1 = v2 & (F1 _V) . v3 = v4 )

( v2 in rng (F1 _V) & v4 in rng (F1 _V) ) by A10, FUNCT_1:3;

then A13: ( v2 is Vertex of G6 & v4 is Vertex of G6 ) ;

then consider F2 being PGraphMapping of G1,G2 such that

A14: F2 = [(F1 _V),((F1 _E) +* (e1 .--> e2))] and

A15: ( F1 is total implies F2 is total ) and

A16: ( F1 is onto implies F2 is onto ) and

A17: ( F1 is one-to-one implies F2 is one-to-one ) by A3, A4, A10, A12, Th152;

take F2 ; :: thesis: ( F2 = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F2 is total ) & ( F0 is onto implies F2 is onto ) & ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )

thus F2 = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] by A5, A14; :: thesis: ( ( F0 is total implies F2 is total ) & ( F0 is onto implies F2 is onto ) & ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )

thus ( F0 is total implies F2 is total ) by A6, A15; :: thesis: ( ( F0 is onto implies F2 is onto ) & ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )

thus ( F0 is onto implies F2 is onto ) by A7, A16; :: thesis: ( ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )

thus ( F0 is one-to-one implies F2 is one-to-one ) by A8, A17; :: thesis: ( F0 is directed implies F2 is directed )

consider F3 being PGraphMapping of G1,G2 such that

A18: F3 = [(F1 _V),((F1 _E) +* (e1 .--> e2))] and

A19: ( F1 is directed implies F3 is directed ) and

( F1 is Disomorphism implies F3 is Disomorphism ) by A3, A4, A10, A12, A13, Th154;

thus ( F0 is directed implies F2 is directed ) by A9, A14, A18, A19; :: thesis: verum

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let v3 be Vertex of G3; :: thesis: for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let v4 be Vertex of G4; :: thesis: for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let e1, e2, v1, v2 be object ; :: thesis: for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let G1 be addAdjVertex of G3,v3,e1,v1; :: thesis: for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let G2 be addAdjVertex of G4,v4,e2,v2; :: thesis: for F0 being PGraphMapping of G3,G4 st 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 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

let F0 be PGraphMapping of G3,G4; :: thesis: ( 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 implies ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) ) )

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: ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

consider G5 being addVertex of G3,v1 such that

A3: G1 is addEdge of G5,v3,e1,v1 by A1, GLIB_006:125;

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

A9: ( 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;

A10: ( v1 in dom (F1 _V) & v3 in dom (F1 _V) & (F1 _V) . v1 = v2 & (F1 _V) . v3 = v4 )

proof

A12:
( not e1 in the_Edges_of G5 & not e2 in the_Edges_of G6 )
by A1, GLIB_006:def 10;
v1 in {v1}
by TARSKI:def 1;

then v1 in dom ({v1} --> v2) ;

then A11: v1 in dom (v1 .--> v2) by FUNCOP_1:def 9;

hence v1 in dom (F1 _V) by A5, FUNCT_4:10, TARSKI:def 3; :: thesis: ( v3 in dom (F1 _V) & (F1 _V) . v1 = v2 & (F1 _V) . v3 = v4 )

thus v3 in dom (F1 _V) by A2, A5, FUNCT_4:10, TARSKI:def 3; :: thesis: ( (F1 _V) . v1 = v2 & (F1 _V) . v3 = v4 )

thus (F1 _V) . v1 = (v1 .--> v2) . v1 by A5, A11, FUNCT_4:13

.= v2 by FUNCOP_1:72 ; :: thesis: (F1 _V) . v3 = v4

v3 <> v1 by A1;

then not v3 in {v1} by TARSKI:def 1;

then not v3 in dom (v1 .--> v2) ;

hence (F1 _V) . v3 = v4 by A2, A5, FUNCT_4:11; :: thesis: verum

end;then v1 in dom ({v1} --> v2) ;

then A11: v1 in dom (v1 .--> v2) by FUNCOP_1:def 9;

hence v1 in dom (F1 _V) by A5, FUNCT_4:10, TARSKI:def 3; :: thesis: ( v3 in dom (F1 _V) & (F1 _V) . v1 = v2 & (F1 _V) . v3 = v4 )

thus v3 in dom (F1 _V) by A2, A5, FUNCT_4:10, TARSKI:def 3; :: thesis: ( (F1 _V) . v1 = v2 & (F1 _V) . v3 = v4 )

thus (F1 _V) . v1 = (v1 .--> v2) . v1 by A5, A11, FUNCT_4:13

.= v2 by FUNCOP_1:72 ; :: thesis: (F1 _V) . v3 = v4

v3 <> v1 by A1;

then not v3 in {v1} by TARSKI:def 1;

then not v3 in dom (v1 .--> v2) ;

hence (F1 _V) . v3 = v4 by A2, A5, FUNCT_4:11; :: thesis: verum

( v2 in rng (F1 _V) & v4 in rng (F1 _V) ) by A10, FUNCT_1:3;

then A13: ( v2 is Vertex of G6 & v4 is Vertex of G6 ) ;

then consider F2 being PGraphMapping of G1,G2 such that

A14: F2 = [(F1 _V),((F1 _E) +* (e1 .--> e2))] and

A15: ( F1 is total implies F2 is total ) and

A16: ( F1 is onto implies F2 is onto ) and

A17: ( F1 is one-to-one implies F2 is one-to-one ) by A3, A4, A10, A12, Th152;

take F2 ; :: thesis: ( F2 = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F2 is total ) & ( F0 is onto implies F2 is onto ) & ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )

thus F2 = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] by A5, A14; :: thesis: ( ( F0 is total implies F2 is total ) & ( F0 is onto implies F2 is onto ) & ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )

thus ( F0 is total implies F2 is total ) by A6, A15; :: thesis: ( ( F0 is onto implies F2 is onto ) & ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )

thus ( F0 is onto implies F2 is onto ) by A7, A16; :: thesis: ( ( F0 is one-to-one implies F2 is one-to-one ) & ( F0 is directed implies F2 is directed ) )

thus ( F0 is one-to-one implies F2 is one-to-one ) by A8, A17; :: thesis: ( F0 is directed implies F2 is directed )

consider F3 being PGraphMapping of G1,G2 such that

A18: F3 = [(F1 _V),((F1 _E) +* (e1 .--> e2))] and

A19: ( F1 is directed implies F3 is directed ) and

( F1 is Disomorphism implies F3 is Disomorphism ) by A3, A4, A10, A12, A13, Th154;

thus ( F0 is directed implies F2 is directed ) by A9, A14, A18, A19; :: thesis: verum