let G1, G2 be _Graph; :: thesis:
let F be PGraphMapping of G1,G2; :: thesis:
let H be Subgraph of G1; :: thesis:
let F9 be PGraphMapping of H, rng (F | H); :: thesis:
assume A1: F9 = F | H ; :: thesis:
then A2: F9 = (rng (F | H)) |` (F | H) by Th86;

hereby :: thesis:

assume not F9 is empty ; :: thesis:
then not F | H is empty by A1;
then ( rng (F9 _V) = the_Vertices_of (rng (F | H)) & rng (F9 _E) = the_Edges_of (rng (F | H)) ) by A1, GLIB_010:54;
hence F9 is onto by GLIB_010:def 12; :: thesis:

end;

hereby :: thesis:

assume F is total ; :: thesis:
then F | H is total by GLIB_010:57;
hence F9 is total by A2, Th87; :: thesis:

end;

thus ( F is one-to-one implies F9 is one-to-one ) by A2; :: thesis:

hereby :: thesis:

assume A3: F is directed ; :: thesis:

now :: thesis:

let e, v, w be object ; :: thesis:
assume A4: ( e in dom (F9 _E) & v in dom (F9 _V) & w in dom (F9 _V) ) ; :: thesis:
then A5: ( (F9 _E) . e = (F _E) . e & (F9 _V) . v = (F _V) . v & (F9 _V) . w = (F _V) . w ) by A1, FUNCT_1:47;
A6: ( v is set & w is set & e is set ) by TARSKI:1;
( dom (F9 _V) = (dom (F _V)) /\ (the_Vertices_of H) & dom (F9 _E) = (dom (F _E)) /\ (the_Edges_of H) ) by A1, GLIB_010:59;
then A7: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) by A4, XBOOLE_0:def 4;
assume e DJoins v,w,H ; :: thesis:
then e DJoins v,w,G1 by A6, GLIB_000:72;
then A8: (F9 _E) . e DJoins (F9 _V) . v,(F9 _V) . w,G2 by A3, A5, A7, GLIB_010:def 14;
(F9 _E) . e in the_Edges_of (rng (F | H))

proof

(F9 _E) . e in rng (F9 _E) by A4, FUNCT_1:3;
hence (F9 _E) . e in the_Edges_of (rng (F | H)) ; :: thesis:

end;

hence (F9 _E) . e DJoins (F9 _V) . v,(F9 _V) . w, rng (F | H) by A8, GLIB_000:73; :: thesis:

end;

hence F9 is directed by GLIB_010:def 14; :: thesis:

end;

hereby :: thesis:

assume A9: F is semi-continuous ; :: thesis:

now :: thesis:

let e, v, w be object ; :: thesis:
assume A10: ( e in dom (F9 _E) & v in dom (F9 _V) & w in dom (F9 _V) ) ; :: thesis:
then A11: ( (F9 _E) . e = (F _E) . e & (F9 _V) . v = (F _V) . v & (F9 _V) . w = (F _V) . w ) by A1, FUNCT_1:47;
assume (F9 _E) . e Joins (F9 _V) . v,(F9 _V) . w, rng (F | H) ; :: thesis:
then A12: (F _E) . e Joins (F _V) . v,(F _V) . w,G2 by A11, GLIB_000:72;
( dom (F9 _V) = (dom (F _V)) /\ (the_Vertices_of H) & dom (F9 _E) = (dom (F _E)) /\ (the_Edges_of H) ) by A1, GLIB_010:59;
then ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) by A10, XBOOLE_0:def 4;
then e Joins v,w,G1 by A9, A12, GLIB_010:def 15;
hence e Joins v,w,H by A10, GLIB_000:73; :: thesis:

end;

hence F9 is semi-continuous by GLIB_010:def 15; :: thesis:

end;

hereby :: thesis:

assume A13: ( F is continuous & F _E is one-to-one ) ; :: thesis:

now :: thesis:

let e9, v, w be object ; :: thesis:
assume A14: ( v in dom (F9 _V) & w in dom (F9 _V) ) ; :: thesis:
then A15: ( (F9 _V) . v = (F _V) . v & (F9 _V) . w = (F _V) . w ) by A1, FUNCT_1:47;
assume A16: e9 Joins (F9 _V) . v,(F9 _V) . w, rng (F | H) ; :: thesis:
then A17: e9 Joins (F _V) . v,(F _V) . w,G2 by A15, GLIB_000:72;
A18: ( dom (F9 _V) = (dom (F _V)) /\ (the_Vertices_of H) & dom (F9 _E) = (dom (F _E)) /\ (the_Edges_of H) ) by A1, GLIB_010:59;
A19: not F | H is empty by A1, A14;
e9 in the_Edges_of (rng (F | H)) by A16, GLIB_000:def 13;
then e9 in rng ((F | H) _E) by A19, GLIB_010:54;
then consider e0 being object such that
A20: ( e0 in dom ((F | H) _E) & ((F | H) _E) . e0 = e9 ) by FUNCT_1:def 3;
( v in dom (F _V) & w in dom (F _V) ) by A14, A18, XBOOLE_0:def 4;
then consider e being object such that
A21: ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A13, A17, GLIB_010:def 16;
take e = e; :: thesis:
A22: ( e0 in dom (F _E) & e0 in the_Edges_of H ) by A1, A18, A20, XBOOLE_0:def 4;
(F _E) . e = (F _E) . e0 by A20, A21, FUNCT_1:49;
then A23: e = e0 by A13, A21, A22, FUNCT_1:def 4;
( e0 is set & v is set & w is set ) by TARSKI:1;
hence e Joins v,w,H by A21, A22, A23, GLIB_000:73; :: thesis:
thus ( e in dom (F9 _E) & (F9 _E) . e = e9 ) by A1, A20, A23; :: thesis:

end;

hence F9 is continuous by GLIB_010:def 16; :: thesis:

end;

hereby :: thesis:

assume A24: F is semi-Dcontinuous ; :: thesis:

now :: thesis:

let e, v, w be object ; :: thesis:
assume A25: ( e in dom (F9 _E) & v in dom (F9 _V) & w in dom (F9 _V) ) ; :: thesis:
then A26: ( (F9 _E) . e = (F _E) . e & (F9 _V) . v = (F _V) . v & (F9 _V) . w = (F _V) . w ) by A1, FUNCT_1:47;
assume (F9 _E) . e DJoins (F9 _V) . v,(F9 _V) . w, rng (F | H) ; :: thesis:
then A27: (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A26, GLIB_000:72;
( dom (F9 _V) = (dom (F _V)) /\ (the_Vertices_of H) & dom (F9 _E) = (dom (F _E)) /\ (the_Edges_of H) ) by A1, GLIB_010:59;
then ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) by A25, XBOOLE_0:def 4;
then e DJoins v,w,G1 by A24, A27, GLIB_010:def 17;
hence e DJoins v,w,H by A25, GLIB_000:73; :: thesis:

end;

hence F9 is semi-Dcontinuous by GLIB_010:def 17; :: thesis:

end;

hereby :: thesis:

assume A28: ( F is Dcontinuous & F _E is one-to-one ) ; :: thesis:

now :: thesis:

let e9, v, w be object ; :: thesis:
assume A29: ( v in dom (F9 _V) & w in dom (F9 _V) ) ; :: thesis:
then A30: ( (F9 _V) . v = (F _V) . v & (F9 _V) . w = (F _V) . w ) by A1, FUNCT_1:47;
assume A31: e9 DJoins (F9 _V) . v,(F9 _V) . w, rng (F | H) ; :: thesis:
then A32: e9 DJoins (F _V) . v,(F _V) . w,G2 by A30, GLIB_000:72;
A33: ( dom (F9 _V) = (dom (F _V)) /\ (the_Vertices_of H) & dom (F9 _E) = (dom (F _E)) /\ (the_Edges_of H) ) by A1, GLIB_010:59;
A34: not F | H is empty by A1, A29;
e9 in the_Edges_of (rng (F | H)) by A31, GLIB_000:def 14;
then e9 in rng ((F | H) _E) by A34, GLIB_010:54;
then consider e0 being object such that
A35: ( e0 in dom ((F | H) _E) & ((F | H) _E) . e0 = e9 ) by FUNCT_1:def 3;
( v in dom (F _V) & w in dom (F _V) ) by A29, A33, XBOOLE_0:def 4;
then consider e being object such that
A36: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A28, A32, GLIB_010:def 18;
take e = e; :: thesis:
A37: ( e0 in dom (F _E) & e0 in the_Edges_of H ) by A1, A33, A35, XBOOLE_0:def 4;
(F _E) . e = (F _E) . e0 by A35, A36, FUNCT_1:49;
then A38: e = e0 by A28, A36, A37, FUNCT_1:def 4;
( e0 is set & v is set & w is set ) by TARSKI:1;
hence e DJoins v,w,H by A36, A37, A38, GLIB_000:73; :: thesis:
thus ( e in dom (F9 _E) & (F9 _E) . e = e9 ) by A1, A35, A38; :: thesis:

end;

hence F9 is Dcontinuous by GLIB_010:def 18; :: thesis:

end;