let G3, G4 be _Graph; :: thesis: for v1, v2 being object

for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2

for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let v1, v2 be object ; :: thesis: for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2

for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let G1 be addVertex of G3,v1; :: thesis: for G2 being addVertex of G4,v2

for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let G2 be addVertex of G4,v2; :: thesis: for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let F0 be PGraphMapping of G3,G4; :: thesis: ( not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 implies ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) ) )

assume A1: ( not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

set f = v1 .--> v2;

A2: dom (v1 .--> v2) = dom ({v1} --> v2) by FUNCOP_1:def 9

.= {v1} \ (the_Vertices_of G3) by A1, ZFMISC_1:59 ;

( v1 is set & v2 is set ) by TARSKI:1;

then rng (v1 .--> v2) = {v2} by FUNCOP_1:88

.= {v2} \ (the_Vertices_of G4) by A1, ZFMISC_1:59 ;

then consider F being PGraphMapping of G1,G2 such that

A3: ( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) ) by A2, Th144;

take F ; :: thesis: ( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

thus ( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) ) by A3; :: thesis: verum

for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2

for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let v1, v2 be object ; :: thesis: for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2

for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let G1 be addVertex of G3,v1; :: thesis: for G2 being addVertex of G4,v2

for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let G2 be addVertex of G4,v2; :: thesis: for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

let F0 be PGraphMapping of G3,G4; :: thesis: ( not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 implies ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) ) )

assume A1: ( not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

set f = v1 .--> v2;

A2: dom (v1 .--> v2) = dom ({v1} --> v2) by FUNCOP_1:def 9

.= {v1} \ (the_Vertices_of G3) by A1, ZFMISC_1:59 ;

( v1 is set & v2 is set ) by TARSKI:1;

then rng (v1 .--> v2) = {v2} by FUNCOP_1:88

.= {v2} \ (the_Vertices_of G4) by A1, ZFMISC_1:59 ;

then consider F being PGraphMapping of G1,G2 such that

A3: ( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) ) by A2, Th144;

take F ; :: thesis: ( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

thus ( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( 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 ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) ) by A3; :: thesis: verum