let G1, G2 be _Graph; :: thesis:
let H be Subgraph of G1; :: thesis:
let F be PGraphMapping of G1,G2; :: thesis:
thus ( F is empty implies F | H is empty ) ; :: thesis:
thus A1: ( F is total implies F | H is total ) :: thesis:

proof

assume A2: F is total ; :: thesis:
A3: dom ((F | H) _V) = (dom (F _V)) /\ (the_Vertices_of H) by RELAT_1:61
.= the_Vertices_of H by A2, XBOOLE_1:28 ;
dom ((F | H) _E) = (dom (F _E)) /\ (the_Edges_of H) by RELAT_1:61
.= the_Edges_of H by A2, XBOOLE_1:28 ;
hence F | H is total by A3; :: thesis:

end;

thus ( F is one-to-one implies F | H is one-to-one ) by FUNCT_1:52; :: thesis:
hence ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) by A1; :: thesis:
thus ( F is semi-continuous implies F | H is semi-continuous ) :: thesis:

proof

assume A4: F is semi-continuous ; :: thesis:
reconsider f = (F _V) | (the_Vertices_of H) as PartFunc of (the_Vertices_of H),(the_Vertices_of G2) by PARTFUN1:10;
reconsider g = (F _E) | (the_Edges_of H) as PartFunc of (the_Edges_of H),(the_Edges_of G2) by PARTFUN1:10;

now :: thesis:

let e, v, w be object ; :: thesis:
assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis:
then A5: ( e in dom (F _E) & e in the_Edges_of H & v in dom (F _V) & v in the_Vertices_of H & w in dom (F _V) & w in the_Vertices_of H ) by RELAT_1:57;
then A6: ( g . e = (F _E) . e & f . v = (F _V) . v & f . w = (F _V) . w ) by FUNCT_1:49;
assume g . e Joins f . v,f . w,G2 ; :: thesis:
then e Joins v,w,G1 by A4, A5, A6;
hence e Joins v,w,H by A5, GLIB_000:73; :: thesis:

end;

hence F | H is semi-continuous ; :: thesis:

end;

( F | H is onto implies F is onto )

proof

assume F | H is onto ; :: thesis:
then ( the_Vertices_of G2 c= rng (F _V) & the_Edges_of G2 c= rng (F _E) ) by RELAT_1:70;
hence F is onto by XBOOLE_0:def 10; :: thesis:

end;

hence ( not F is onto implies not F | H is onto ) ; :: thesis:
thus ( F is directed implies F | H is directed ) :: thesis:

proof

assume A7: F is directed ; :: thesis:
let e, v, w be object ; :: according to GLIB_010:def 14 :: thesis:
assume ( e in dom ((F | H) _E) & v in dom ((F | H) _V) & w in dom ((F | H) _V) ) ; :: thesis:
then A8: ( e in dom (F _E) & e in the_Edges_of H & v in dom (F _V) & v in the_Vertices_of H & w in dom (F _V) & w in the_Vertices_of H ) by RELAT_1:57;
then A9: ( ((F | H) _E) . e = (F _E) . e & ((F | H) _V) . v = (F _V) . v & ((F | H) _V) . w = (F _V) . w ) by FUNCT_1:49;
assume A10: e DJoins v,w,H ; :: thesis:
( v is set & w is set ) by TARSKI:1;
then e DJoins v,w,G1 by A10, GLIB_000:72;
hence ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2 by A7, A8, A9; :: thesis:

end;

thus ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) :: thesis:

proof

assume A11: F is semi-Dcontinuous ; :: thesis:
let e, v, w be object ; :: according to GLIB_010:def 17 :: thesis:
assume ( e in dom ((F | H) _E) & v in dom ((F | H) _V) & w in dom ((F | H) _V) ) ; :: thesis:
then A12: ( e in dom (F _E) & e in the_Edges_of H & v in dom (F _V) & v in the_Vertices_of H & w in dom (F _V) & w in the_Vertices_of H ) by RELAT_1:57;
then A13: ( ((F | H) _E) . e = (F _E) . e & ((F | H) _V) . v = (F _V) . v & ((F | H) _V) . w = (F _V) . w ) by FUNCT_1:49;
assume ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2 ; :: thesis:
then e DJoins v,w,G1 by A11, A12, A13;
hence e DJoins v,w,H by A12, GLIB_000:73; :: thesis:

end;