now :: thesis:

hereby :: thesis:

let e be object ; :: thesis:
assume A10: e in dom g ; :: thesis:
( (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:

end;

let e, v, w be object ; :: thesis:
assume A12: ( e in dom g & v in dom h & w in dom h & e Joins v,w,G1 ) ; :: thesis:
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:

end;

then reconsider F = [h,g] as PGraphMapping of G1,G2 by Th8;
take F ; :: thesis:
thus F = [((F0 _V) +* f),(F0 _E)] ; :: thesis:
thus ( not F0 is empty implies not F is empty ) by FUNCT_4:10, XBOOLE_1:3; :: thesis:
thus ( F0 is total implies F is total ) :: thesis:

proof

assume F0 is total ; :: thesis:
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:

end;

thus ( F0 is onto implies F is onto ) :: thesis:

proof

assume F0 is onto ; :: thesis:
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:

end;

thus ( F0 is one-to-one implies F is one-to-one ) by A8, FUNCT_4:92; :: thesis:
thus ( F0 is directed implies F is directed ) :: thesis:

proof

assume A18: F0 is directed ; :: thesis:

now :: thesis:

let e, v, w be object ; :: thesis:
assume A19: ( e in dom g & v in dom h & w in dom h & e DJoins v,w,G1 ) ; :: thesis:
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:

end;

hence F is directed ; :: thesis:

end;

thus ( F0 is semi-continuous implies F is semi-continuous ) :: thesis:

proof

assume A23: F0 is semi-continuous ; :: thesis:

now :: thesis:

let e, v, w be object ; :: thesis:
assume A24: ( e in dom g & v in dom h & w in dom h & g . e Joins h . v,h . w,G2 ) ; :: thesis:
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

assume ( v in dom f or w in dom f ) ; :: thesis:

per cases ;

suppose v in dom f ; :: thesis:

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

end;

suppose w in dom f ; :: thesis:

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

end;

( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) ) by A24, FUNCT_4:def 1;
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:

end;

hence F is semi-continuous ; :: thesis:

end;

thus ( F0 is continuous implies F is continuous ) :: thesis:

proof

assume A30: F0 is continuous ; :: thesis:

now :: thesis:

let e9, v, w be object ; :: thesis:
assume A31: ( v in dom h & w in dom h & e9 Joins h . v,h . w,G2 ) ; :: thesis:
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

assume ( v in dom f or w in dom f ) ; :: thesis:

per cases ;

suppose v in dom f ; :: thesis:

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

end;

suppose w in dom f ; :: thesis:

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

end;

( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) ) by A31, FUNCT_4:def 1;
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:
( v is set & w is set ) by TARSKI:1;
hence e Joins v,w,G1 by A36, GLIB_009:41; :: thesis:
thus ( e in dom g & g . e = e9 ) by A36; :: thesis:

end;

hence F is continuous ; :: thesis:

end;

thus ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) :: thesis:

proof

assume A37: F0 is semi-Dcontinuous ; :: thesis:

now :: thesis:

let e, v, w be object ; :: thesis:
assume A38: ( e in dom g & v in dom h & w in dom h & g . e DJoins h . v,h . w,G2 ) ; :: thesis:
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

assume ( v in dom f or w in dom f ) ; :: thesis:

per cases ;

suppose v in dom f ; :: thesis:

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

end;

suppose w in dom f ; :: thesis:

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

end;

( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) ) by A38, FUNCT_4:def 1;
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:

end;

hence F is semi-Dcontinuous ; :: thesis:

end;

thus ( F0 is Dcontinuous implies F is Dcontinuous ) :: thesis:

proof

assume A44: F0 is Dcontinuous ; :: thesis:

now :: thesis:

let e9, v, w be object ; :: thesis:
assume A45: ( v in dom h & w in dom h & e9 DJoins h . v,h . w,G2 ) ; :: thesis:
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

assume ( v in dom f or w in dom f ) ; :: thesis:

per cases ;

suppose v in dom f ; :: thesis:

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

end;

suppose w in dom f ; :: thesis:

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

end;

( v in (dom (F0 _V)) \/ (dom f) & w in (dom (F0 _V)) \/ (dom f) ) by A45, FUNCT_4:def 1;
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:
( v is set & w is set ) by TARSKI:1;
hence e DJoins v,w,G1 by A50, GLIB_009:41; :: thesis:
thus ( e in dom g & g . e = e9 ) by A50; :: thesis:

end;

hence F is Dcontinuous ; :: thesis:

end;