let G3, G4 be _Graph; :: thesis: for V1, V2 being set

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

let V1, V2 be set ; :: thesis: for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

let G1 be addVertices of G3,V1; :: thesis: for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

let G2 be addVertices of G4,V2; :: thesis: for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

let F0 be PGraphMapping of G3,G4; :: thesis: for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

let f be one-to-one Function; :: thesis: ( dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) implies ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) ) )

assume A1: ( dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

set h = (F0 _V) +* f;

A2: dom ((F0 _V) +* f) = (dom (F0 _V)) \/ (V1 \ (the_Vertices_of G3)) by A1, FUNCT_4:def 1;

dom ((F0 _V) +* f) c= (the_Vertices_of G3) \/ V1 by A2, XBOOLE_1:13;

then A3: dom ((F0 _V) +* f) c= the_Vertices_of G1 by GLIB_006:def 10;

(rng (F0 _V)) \/ (rng f) c= (the_Vertices_of G4) \/ V2 by A1, XBOOLE_1:13;

then A4: (rng (F0 _V)) \/ (rng f) c= the_Vertices_of G2 by GLIB_006:def 10;

rng ((F0 _V) +* f) c= (rng (F0 _V)) \/ (rng f) by FUNCT_4:17;

then rng ((F0 _V) +* f) c= the_Vertices_of G2 by A4, XBOOLE_1:1;

then reconsider h = (F0 _V) +* f as PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) by A3, RELSET_1:4;

( the_Edges_of G1 = the_Edges_of G3 & the_Edges_of G2 = the_Edges_of G4 ) by GLIB_006:def 10;

then reconsider g = F0 _E as PartFunc of (the_Edges_of G1),(the_Edges_of G2) ;

A5: (dom f) /\ (the_Vertices_of G3) = {} by A1, XBOOLE_1:79, XBOOLE_0:def 7;

(dom (F0 _V)) /\ (dom f) c= (dom f) /\ (the_Vertices_of G3) by XBOOLE_1:26;

then A6: dom (F0 _V) misses dom f by A5, XBOOLE_1:3, XBOOLE_0:def 7;

A7: (rng f) /\ (the_Vertices_of G4) = {} by A1, XBOOLE_1:79, XBOOLE_0:def 7;

(rng (F0 _V)) /\ (rng f) c= (rng f) /\ (the_Vertices_of G4) by XBOOLE_1:26;

then A8: rng (F0 _V) misses rng f by A7, XBOOLE_1:3, XBOOLE_0:def 7;

A9: (dom h) /\ (the_Vertices_of G3) = ((dom (F0 _V)) \/ (dom f)) /\ (the_Vertices_of G3) by FUNCT_4:def 1

.= ((dom (F0 _V)) /\ (the_Vertices_of G3)) \/ ((dom f) /\ (the_Vertices_of G3)) by XBOOLE_1:23

.= dom (F0 _V) by A5, XBOOLE_1:28 ;

take F ; :: thesis: ( F = [((F0 _V) +* f),(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 ) )

thus F = [((F0 _V) +* f),(F0 _E)] ; :: thesis: ( ( 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 ) )

thus ( not F0 is empty implies not F is empty ) by FUNCT_4:10, XBOOLE_1:3; :: thesis: ( ( 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 ( F0 is total implies F is total ) :: thesis: ( ( 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 ( F0 is directed implies F is directed ) :: thesis: ( ( 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 ) )

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

let V1, V2 be set ; :: thesis: for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

let G1 be addVertices of G3,V1; :: thesis: for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

let G2 be addVertices of G4,V2; :: thesis: for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

let F0 be PGraphMapping of G3,G4; :: thesis: for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

let f be one-to-one Function; :: thesis: ( dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) implies ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) ) )

assume A1: ( dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(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 ) )

set h = (F0 _V) +* f;

A2: dom ((F0 _V) +* f) = (dom (F0 _V)) \/ (V1 \ (the_Vertices_of G3)) by A1, FUNCT_4:def 1;

dom ((F0 _V) +* f) c= (the_Vertices_of G3) \/ V1 by A2, XBOOLE_1:13;

then A3: dom ((F0 _V) +* f) c= the_Vertices_of G1 by GLIB_006:def 10;

(rng (F0 _V)) \/ (rng f) c= (the_Vertices_of G4) \/ V2 by A1, XBOOLE_1:13;

then A4: (rng (F0 _V)) \/ (rng f) c= the_Vertices_of G2 by GLIB_006:def 10;

rng ((F0 _V) +* f) c= (rng (F0 _V)) \/ (rng f) by FUNCT_4:17;

then rng ((F0 _V) +* f) c= the_Vertices_of G2 by A4, XBOOLE_1:1;

then reconsider h = (F0 _V) +* f as PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) by A3, RELSET_1:4;

( the_Edges_of G1 = the_Edges_of G3 & the_Edges_of G2 = the_Edges_of G4 ) by GLIB_006:def 10;

then reconsider g = F0 _E as PartFunc of (the_Edges_of G1),(the_Edges_of G2) ;

A5: (dom f) /\ (the_Vertices_of G3) = {} by A1, XBOOLE_1:79, XBOOLE_0:def 7;

(dom (F0 _V)) /\ (dom f) c= (dom f) /\ (the_Vertices_of G3) by XBOOLE_1:26;

then A6: dom (F0 _V) misses dom f by A5, XBOOLE_1:3, XBOOLE_0:def 7;

A7: (rng f) /\ (the_Vertices_of G4) = {} by A1, XBOOLE_1:79, XBOOLE_0:def 7;

(rng (F0 _V)) /\ (rng f) c= (rng f) /\ (the_Vertices_of G4) by XBOOLE_1:26;

then A8: rng (F0 _V) misses rng f by A7, XBOOLE_1:3, XBOOLE_0:def 7;

A9: (dom h) /\ (the_Vertices_of G3) = ((dom (F0 _V)) \/ (dom f)) /\ (the_Vertices_of G3) by FUNCT_4:def 1

.= ((dom (F0 _V)) /\ (the_Vertices_of G3)) \/ ((dom f) /\ (the_Vertices_of G3)) by XBOOLE_1:23

.= dom (F0 _V) by A5, XBOOLE_1:28 ;

now :: thesis: ( ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom h & (the_Target_of G1) . e in dom h ) ) & ( for e, v, w being object st e in dom g & v in dom h & w in dom h & e Joins v,w,G1 holds

g . e Joins h . v,h . w,G2 ) )

assume A12: ( e in dom g & v in dom h & w in dom h & e Joins v,w,G1 ) ; :: thesis: g . e Joins h . v,h . w,G2

A13: e Joins v,w,G3 by A12, GLIB_009:41;

then A14: ( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) by GLIB_000:13;

then ( v in dom (F0 _V) & w in dom (F0 _V) ) by A12, A9, XBOOLE_0:def 4;

then (F0 _E) . e Joins (F0 _V) . v,(F0 _V) . w,G4 by A12, A13, Th4;

then A15: g . e Joins (F0 _V) . v,(F0 _V) . w,G2 by GLIB_009:41;

( not v in dom f & not w in dom f ) by A1, A14, XBOOLE_0:def 5;

then ( h . v = (F0 _V) . v & h . w = (F0 _V) . w ) by FUNCT_4:11;

hence g . e Joins h . v,h . w,G2 by A15; :: thesis: verum

end;

then reconsider F = [h,g] as PGraphMapping of G1,G2 by Th8;( (the_Source_of G1) . e in dom h & (the_Target_of G1) . e in dom h ) ) & ( for e, v, w being object st e in dom g & v in dom h & w in dom h & e Joins v,w,G1 holds

g . e Joins h . v,h . w,G2 ) )

hereby :: thesis: for e, v, w being object st e in dom g & v in dom h & w in dom h & e Joins v,w,G1 holds

g . e Joins h . v,h . w,G2

let e, v, w be object ; :: thesis: ( e in dom g & v in dom h & w in dom h & e Joins v,w,G1 implies g . e Joins h . v,h . w,G2 )g . e Joins h . v,h . w,G2

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of G1) . e in dom h & (the_Target_of G1) . e in dom h ) )

assume A10: e in dom g ; :: thesis: ( (the_Source_of G1) . e in dom h & (the_Target_of G1) . e in dom h )

( (the_Source_of G1) . e = (the_Source_of G3) . e & (the_Target_of G1) . e = (the_Target_of G3) . e ) by GLIB_006:def 10;

then A11: ( (the_Source_of G1) . e in dom (F0 _V) & (the_Target_of G1) . e in dom (F0 _V) ) by A10, Th5;

dom (F0 _V) c= dom h by FUNCT_4:10;

hence ( (the_Source_of G1) . e in dom h & (the_Target_of G1) . e in dom h ) by A11; :: thesis: verum

end;assume A10: e in dom g ; :: thesis: ( (the_Source_of G1) . e in dom h & (the_Target_of G1) . e in dom h )

( (the_Source_of G1) . e = (the_Source_of G3) . e & (the_Target_of G1) . e = (the_Target_of G3) . e ) by GLIB_006:def 10;

then A11: ( (the_Source_of G1) . e in dom (F0 _V) & (the_Target_of G1) . e in dom (F0 _V) ) by A10, Th5;

dom (F0 _V) c= dom h by FUNCT_4:10;

hence ( (the_Source_of G1) . e in dom h & (the_Target_of G1) . e in dom h ) by A11; :: thesis: verum

assume A12: ( e in dom g & v in dom h & w in dom h & e Joins v,w,G1 ) ; :: thesis: g . e Joins h . v,h . w,G2

A13: e Joins v,w,G3 by A12, GLIB_009:41;

then A14: ( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) by GLIB_000:13;

then ( v in dom (F0 _V) & w in dom (F0 _V) ) by A12, A9, XBOOLE_0:def 4;

then (F0 _E) . e Joins (F0 _V) . v,(F0 _V) . w,G4 by A12, A13, Th4;

then A15: g . e Joins (F0 _V) . v,(F0 _V) . w,G2 by GLIB_009:41;

( not v in dom f & not w in dom f ) by A1, A14, XBOOLE_0:def 5;

then ( h . v = (F0 _V) . v & h . w = (F0 _V) . w ) by FUNCT_4:11;

hence g . e Joins h . v,h . w,G2 by A15; :: thesis: verum

take F ; :: thesis: ( F = [((F0 _V) +* f),(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 ) )

thus F = [((F0 _V) +* f),(F0 _E)] ; :: thesis: ( ( 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 ) )

thus ( not F0 is empty implies not F is empty ) by FUNCT_4:10, XBOOLE_1:3; :: thesis: ( ( 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 ( F0 is total implies F is total ) :: thesis: ( ( 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 ) )

proof

thus
( F0 is onto implies F is onto )
:: thesis: ( ( 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
F0 is total
; :: thesis: F is total

then A16: ( dom (F0 _V) = the_Vertices_of G3 & dom (F0 _E) = the_Edges_of G3 ) ;

then dom h = (the_Vertices_of G3) \/ (V1 \ (the_Vertices_of G3)) by A1, FUNCT_4:def 1

.= (the_Vertices_of G3) \/ V1 by XBOOLE_1:39

.= the_Vertices_of G1 by GLIB_006:def 10 ;

hence F is total by A16, GLIB_006:def 10; :: thesis: verum

end;then A16: ( dom (F0 _V) = the_Vertices_of G3 & dom (F0 _E) = the_Edges_of G3 ) ;

then dom h = (the_Vertices_of G3) \/ (V1 \ (the_Vertices_of G3)) by A1, FUNCT_4:def 1

.= (the_Vertices_of G3) \/ V1 by XBOOLE_1:39

.= the_Vertices_of G1 by GLIB_006:def 10 ;

hence F is total by A16, GLIB_006:def 10; :: thesis: verum

proof

thus
( F0 is one-to-one implies F is one-to-one )
by A8, FUNCT_4:92; :: thesis: ( ( 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
F0 is onto
; :: thesis: F is onto

then A17: ( rng (F0 _V) = the_Vertices_of G4 & rng (F0 _E) = the_Edges_of G4 ) ;

rng h = (rng (F0 _V)) \/ (rng f) by A6, NECKLACE:6

.= (the_Vertices_of G4) \/ V2 by A1, A17, XBOOLE_1:39

.= the_Vertices_of G2 by GLIB_006:def 10 ;

hence F is onto by A17, GLIB_006:def 10; :: thesis: verum

end;then A17: ( rng (F0 _V) = the_Vertices_of G4 & rng (F0 _E) = the_Edges_of G4 ) ;

rng h = (rng (F0 _V)) \/ (rng f) by A6, NECKLACE:6

.= (the_Vertices_of G4) \/ V2 by A1, A17, XBOOLE_1:39

.= the_Vertices_of G2 by GLIB_006:def 10 ;

hence F is onto by A17, GLIB_006:def 10; :: thesis: verum

thus ( F0 is directed implies F is directed ) :: thesis: ( ( 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 ) )

proof

thus
( F0 is semi-continuous implies F is semi-continuous )
:: thesis: ( ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
assume A18:
F0 is directed
; :: thesis: F is directed

end;now :: thesis: for e, v, w being object st e in dom g & v in dom h & w in dom h & e DJoins v,w,G1 holds

g . e DJoins h . v,h . w,G2

hence
F is directed
; :: thesis: verumg . e DJoins h . v,h . w,G2

let e, v, w be object ; :: thesis: ( e in dom g & v in dom h & w in dom h & e DJoins v,w,G1 implies g . e DJoins h . v,h . w,G2 )

assume A19: ( e in dom g & v in dom h & w in dom h & e DJoins v,w,G1 ) ; :: thesis: g . e DJoins h . v,h . w,G2

A20: e DJoins v,w,G3 by A19, GLIB_009:41;

then e Joins v,w,G3 by GLIB_000:16;

then A21: ( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) by GLIB_000:13;

then ( v in dom (F0 _V) & w in dom (F0 _V) ) by A19, A9, XBOOLE_0:def 4;

then (F0 _E) . e DJoins (F0 _V) . v,(F0 _V) . w,G4 by A18, A19, A20;

then A22: g . e DJoins (F0 _V) . v,(F0 _V) . w,G2 by GLIB_009:41;

( not v in dom f & not w in dom f ) by A1, A21, XBOOLE_0:def 5;

then ( h . v = (F0 _V) . v & h . w = (F0 _V) . w ) by FUNCT_4:11;

hence g . e DJoins h . v,h . w,G2 by A22; :: thesis: verum

end;assume A19: ( e in dom g & v in dom h & w in dom h & e DJoins v,w,G1 ) ; :: thesis: g . e DJoins h . v,h . w,G2

A20: e DJoins v,w,G3 by A19, GLIB_009:41;

then e Joins v,w,G3 by GLIB_000:16;

then A21: ( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) by GLIB_000:13;

then ( v in dom (F0 _V) & w in dom (F0 _V) ) by A19, A9, XBOOLE_0:def 4;

then (F0 _E) . e DJoins (F0 _V) . v,(F0 _V) . w,G4 by A18, A19, A20;

then A22: g . e DJoins (F0 _V) . v,(F0 _V) . w,G2 by GLIB_009:41;

( not v in dom f & not w in dom f ) by A1, A21, XBOOLE_0:def 5;

then ( h . v = (F0 _V) . v & h . w = (F0 _V) . w ) by FUNCT_4:11;

hence g . e DJoins h . v,h . w,G2 by A22; :: thesis: verum

proof

thus
( F0 is continuous implies F is continuous )
:: thesis: ( ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )
assume A23:
F0 is semi-continuous
; :: thesis: F is semi-continuous

end;now :: thesis: for e, v, w being object st e in dom g & v in dom h & w in dom h & g . e Joins h . v,h . w,G2 holds

e Joins v,w,G1

hence
F is semi-continuous
; :: thesis: verume Joins v,w,G1

let e, v, w be object ; :: thesis: ( e in dom g & v in dom h & w in dom h & g . e Joins h . v,h . w,G2 implies e Joins v,w,G1 )

assume A24: ( e in dom g & v in dom h & w in dom h & g . e Joins h . v,h . w,G2 ) ; :: thesis: e Joins v,w,G1

then A25: (F0 _E) . e Joins h . v,h . w,G4 by GLIB_009:41;

then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;

then A26: ( not h . v in rng f & not h . w in rng f ) by A7, XBOOLE_0:def 4;

A27: ( not v in dom f & not w in dom f )

then A28: ( v in dom (F0 _V) & w in dom (F0 _V) ) by A27, XBOOLE_0:def 3;

( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by A27, FUNCT_4:11;

then (F0 _E) . e Joins (F0 _V) . v,(F0 _V) . w,G4 by A25;

then A29: e Joins v,w,G3 by A23, A24, A28;

( v is set & w is set ) by TARSKI:1;

hence e Joins v,w,G1 by A29, GLIB_009:41; :: thesis: verum

end;assume A24: ( e in dom g & v in dom h & w in dom h & g . e Joins h . v,h . w,G2 ) ; :: thesis: e Joins v,w,G1

then A25: (F0 _E) . e Joins h . v,h . w,G4 by GLIB_009:41;

then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;

then A26: ( not h . v in rng f & not h . w in rng f ) by A7, XBOOLE_0:def 4;

A27: ( not v in dom f & not w in dom f )

proof

( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) )
by A24, FUNCT_4:def 1;
assume
( v in dom f or w in dom f )
; :: thesis: contradiction

end;per cases then
( v in dom f or w in dom f )
;

end;

suppose
v in dom f
; :: thesis: contradiction

then
( f . v in rng f & h . v = f . v )
by FUNCT_1:3, FUNCT_4:13;

hence contradiction by A26; :: thesis: verum

end;hence contradiction by A26; :: thesis: verum

suppose
w in dom f
; :: thesis: contradiction

then
( f . w in rng f & h . w = f . w )
by FUNCT_1:3, FUNCT_4:13;

hence contradiction by A26; :: thesis: verum

end;hence contradiction by A26; :: thesis: verum

then A28: ( v in dom (F0 _V) & w in dom (F0 _V) ) by A27, XBOOLE_0:def 3;

( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by A27, FUNCT_4:11;

then (F0 _E) . e Joins (F0 _V) . v,(F0 _V) . w,G4 by A25;

then A29: e Joins v,w,G3 by A23, A24, A28;

( v is set & w is set ) by TARSKI:1;

hence e Joins v,w,G1 by A29, GLIB_009:41; :: thesis: verum

proof

thus
( F0 is semi-Dcontinuous implies F is semi-Dcontinuous )
:: thesis: ( F0 is Dcontinuous implies F is Dcontinuous )
assume A30:
F0 is continuous
; :: thesis: F is continuous

end;now :: thesis: for e9, v, w being object st v in dom h & w in dom h & e9 Joins h . v,h . w,G2 holds

ex e being object st

( e Joins v,w,G1 & e in dom g & g . e = e9 )

hence
F is continuous
; :: thesis: verumex e being object st

( e Joins v,w,G1 & e in dom g & g . e = e9 )

let e9, v, w be object ; :: thesis: ( v in dom h & w in dom h & e9 Joins h . v,h . w,G2 implies ex e being object st

( e Joins v,w,G1 & e in dom g & g . e = e9 ) )

assume A31: ( v in dom h & w in dom h & e9 Joins h . v,h . w,G2 ) ; :: thesis: ex e being object st

( e Joins v,w,G1 & e in dom g & g . e = e9 )

then A32: e9 Joins h . v,h . w,G4 by GLIB_009:41;

then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;

then A33: ( not h . v in rng f & not h . w in rng f ) by A7, XBOOLE_0:def 4;

A34: ( not v in dom f & not w in dom f )

then A35: ( v in dom (F0 _V) & w in dom (F0 _V) ) by A34, XBOOLE_0:def 3;

( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by A34, FUNCT_4:11;

then consider e being object such that

A36: ( e Joins v,w,G3 & e in dom (F _E) & (F _E) . e = e9 ) by A30, A32, A35;

take e = e; :: thesis: ( e Joins v,w,G1 & e in dom g & g . e = e9 )

( v is set & w is set ) by TARSKI:1;

hence e Joins v,w,G1 by A36, GLIB_009:41; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A36; :: thesis: verum

end;( e Joins v,w,G1 & e in dom g & g . e = e9 ) )

assume A31: ( v in dom h & w in dom h & e9 Joins h . v,h . w,G2 ) ; :: thesis: ex e being object st

( e Joins v,w,G1 & e in dom g & g . e = e9 )

then A32: e9 Joins h . v,h . w,G4 by GLIB_009:41;

then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;

then A33: ( not h . v in rng f & not h . w in rng f ) by A7, XBOOLE_0:def 4;

A34: ( not v in dom f & not w in dom f )

proof

( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) )
by A31, FUNCT_4:def 1;
assume
( v in dom f or w in dom f )
; :: thesis: contradiction

end;per cases then
( v in dom f or w in dom f )
;

end;

suppose
v in dom f
; :: thesis: contradiction

then
( f . v in rng f & h . v = f . v )
by FUNCT_1:3, FUNCT_4:13;

hence contradiction by A33; :: thesis: verum

end;hence contradiction by A33; :: thesis: verum

suppose
w in dom f
; :: thesis: contradiction

then
( f . w in rng f & h . w = f . w )
by FUNCT_1:3, FUNCT_4:13;

hence contradiction by A33; :: thesis: verum

end;hence contradiction by A33; :: thesis: verum

then A35: ( v in dom (F0 _V) & w in dom (F0 _V) ) by A34, XBOOLE_0:def 3;

( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by A34, FUNCT_4:11;

then consider e being object such that

A36: ( e Joins v,w,G3 & e in dom (F _E) & (F _E) . e = e9 ) by A30, A32, A35;

take e = e; :: thesis: ( e Joins v,w,G1 & e in dom g & g . e = e9 )

( v is set & w is set ) by TARSKI:1;

hence e Joins v,w,G1 by A36, GLIB_009:41; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A36; :: thesis: verum

proof

thus
( F0 is Dcontinuous implies F is Dcontinuous )
:: thesis: verum
assume A37:
F0 is semi-Dcontinuous
; :: thesis: F is semi-Dcontinuous

end;now :: thesis: for e, v, w being object st e in dom g & v in dom h & w in dom h & g . e DJoins h . v,h . w,G2 holds

e DJoins v,w,G1

hence
F is semi-Dcontinuous
; :: thesis: verume DJoins v,w,G1

let e, v, w be object ; :: thesis: ( e in dom g & v in dom h & w in dom h & g . e DJoins h . v,h . w,G2 implies e DJoins v,w,G1 )

assume A38: ( e in dom g & v in dom h & w in dom h & g . e DJoins h . v,h . w,G2 ) ; :: thesis: e DJoins v,w,G1

then A39: (F0 _E) . e DJoins h . v,h . w,G4 by GLIB_009:41;

then (F0 _E) . e Joins h . v,h . w,G4 by GLIB_000:16;

then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;

then A40: ( not h . v in rng f & not h . w in rng f ) by A7, XBOOLE_0:def 4;

A41: ( not v in dom f & not w in dom f )

then A42: ( v in dom (F0 _V) & w in dom (F0 _V) ) by A41, XBOOLE_0:def 3;

( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by A41, FUNCT_4:11;

then (F0 _E) . e DJoins (F0 _V) . v,(F0 _V) . w,G4 by A39;

then A43: e DJoins v,w,G3 by A37, A38, A42;

( v is set & w is set ) by TARSKI:1;

hence e DJoins v,w,G1 by A43, GLIB_009:41; :: thesis: verum

end;assume A38: ( e in dom g & v in dom h & w in dom h & g . e DJoins h . v,h . w,G2 ) ; :: thesis: e DJoins v,w,G1

then A39: (F0 _E) . e DJoins h . v,h . w,G4 by GLIB_009:41;

then (F0 _E) . e Joins h . v,h . w,G4 by GLIB_000:16;

then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;

then A40: ( not h . v in rng f & not h . w in rng f ) by A7, XBOOLE_0:def 4;

A41: ( not v in dom f & not w in dom f )

proof

( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) )
by A38, FUNCT_4:def 1;
assume
( v in dom f or w in dom f )
; :: thesis: contradiction

end;per cases then
( v in dom f or w in dom f )
;

end;

suppose
v in dom f
; :: thesis: contradiction

then
( f . v in rng f & h . v = f . v )
by FUNCT_1:3, FUNCT_4:13;

hence contradiction by A40; :: thesis: verum

end;hence contradiction by A40; :: thesis: verum

suppose
w in dom f
; :: thesis: contradiction

then
( f . w in rng f & h . w = f . w )
by FUNCT_1:3, FUNCT_4:13;

hence contradiction by A40; :: thesis: verum

end;hence contradiction by A40; :: thesis: verum

then A42: ( v in dom (F0 _V) & w in dom (F0 _V) ) by A41, XBOOLE_0:def 3;

( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by A41, FUNCT_4:11;

then (F0 _E) . e DJoins (F0 _V) . v,(F0 _V) . w,G4 by A39;

then A43: e DJoins v,w,G3 by A37, A38, A42;

( v is set & w is set ) by TARSKI:1;

hence e DJoins v,w,G1 by A43, GLIB_009:41; :: thesis: verum

proof

assume A44:
F0 is Dcontinuous
; :: thesis: F is Dcontinuous

end;now :: thesis: for e9, v, w being object st v in dom h & w in dom h & e9 DJoins h . v,h . w,G2 holds

ex e being object st

( e DJoins v,w,G1 & e in dom g & g . e = e9 )

hence
F is Dcontinuous
; :: thesis: verumex e being object st

( e DJoins v,w,G1 & e in dom g & g . e = e9 )

let e9, v, w be object ; :: thesis: ( v in dom h & w in dom h & e9 DJoins h . v,h . w,G2 implies ex e being object st

( e DJoins v,w,G1 & e in dom g & g . e = e9 ) )

assume A45: ( v in dom h & w in dom h & e9 DJoins h . v,h . w,G2 ) ; :: thesis: ex e being object st

( e DJoins v,w,G1 & e in dom g & g . e = e9 )

then A46: e9 DJoins h . v,h . w,G4 by GLIB_009:41;

then e9 Joins h . v,h . w,G4 by GLIB_000:16;

then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;

then A47: ( not h . v in rng f & not h . w in rng f ) by A7, XBOOLE_0:def 4;

A48: ( not v in dom f & not w in dom f )

then A49: ( v in dom (F0 _V) & w in dom (F0 _V) ) by A48, XBOOLE_0:def 3;

( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by A48, FUNCT_4:11;

then consider e being object such that

A50: ( e DJoins v,w,G3 & e in dom (F _E) & (F _E) . e = e9 ) by A44, A46, A49;

take e = e; :: thesis: ( e DJoins v,w,G1 & e in dom g & g . e = e9 )

( v is set & w is set ) by TARSKI:1;

hence e DJoins v,w,G1 by A50, GLIB_009:41; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A50; :: thesis: verum

end;( e DJoins v,w,G1 & e in dom g & g . e = e9 ) )

assume A45: ( v in dom h & w in dom h & e9 DJoins h . v,h . w,G2 ) ; :: thesis: ex e being object st

( e DJoins v,w,G1 & e in dom g & g . e = e9 )

then A46: e9 DJoins h . v,h . w,G4 by GLIB_009:41;

then e9 Joins h . v,h . w,G4 by GLIB_000:16;

then ( h . v in the_Vertices_of G4 & h . w in the_Vertices_of G4 ) by GLIB_000:13;

then A47: ( not h . v in rng f & not h . w in rng f ) by A7, XBOOLE_0:def 4;

A48: ( not v in dom f & not w in dom f )

proof

( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) )
by A45, FUNCT_4:def 1;
assume
( v in dom f or w in dom f )
; :: thesis: contradiction

end;per cases then
( v in dom f or w in dom f )
;

end;

suppose
v in dom f
; :: thesis: contradiction

then
( f . v in rng f & h . v = f . v )
by FUNCT_1:3, FUNCT_4:13;

hence contradiction by A47; :: thesis: verum

end;hence contradiction by A47; :: thesis: verum

suppose
w in dom f
; :: thesis: contradiction

then
( f . w in rng f & h . w = f . w )
by FUNCT_1:3, FUNCT_4:13;

hence contradiction by A47; :: thesis: verum

end;hence contradiction by A47; :: thesis: verum

then A49: ( v in dom (F0 _V) & w in dom (F0 _V) ) by A48, XBOOLE_0:def 3;

( (F0 _V) . v = h . v & (F0 _V) . w = h . w ) by A48, FUNCT_4:11;

then consider e being object such that

A50: ( e DJoins v,w,G3 & e in dom (F _E) & (F _E) . e = e9 ) by A44, A46, A49;

take e = e; :: thesis: ( e DJoins v,w,G1 & e in dom g & g . e = e9 )

( v is set & w is set ) by TARSKI:1;

hence e DJoins v,w,G1 by A50, GLIB_009:41; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A50; :: thesis: verum