let G1, G2 be _Graph; :: thesis: for H being Subgraph of G1

for F being PGraphMapping of G1,G2 holds

( ( F is empty implies F | H is empty ) & ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

let H be Subgraph of G1; :: thesis: for F being PGraphMapping of G1,G2 holds

( ( F is empty implies F | H is empty ) & ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

let F be PGraphMapping of G1,G2; :: thesis: ( ( F is empty implies F | H is empty ) & ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

thus ( F is empty implies F | H is empty ) ; :: thesis: ( ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

thus A1: ( F is total implies F | H is total ) :: thesis: ( ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

hence ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) by A1; :: thesis: ( ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

thus ( F is semi-continuous implies F | H is semi-continuous ) :: thesis: ( ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

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

for F being PGraphMapping of G1,G2 holds

( ( F is empty implies F | H is empty ) & ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

let H be Subgraph of G1; :: thesis: for F being PGraphMapping of G1,G2 holds

( ( F is empty implies F | H is empty ) & ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

let F be PGraphMapping of G1,G2; :: thesis: ( ( F is empty implies F | H is empty ) & ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

thus ( F is empty implies F | H is empty ) ; :: thesis: ( ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

thus A1: ( F is total implies F | H is total ) :: thesis: ( ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

proof

thus
( F is one-to-one implies F | H is one-to-one )
by FUNCT_1:52; :: thesis: ( ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )
assume A2:
F is total
; :: thesis: F | H is total

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: verum

end;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: verum

hence ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) by A1; :: thesis: ( ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

thus ( F is semi-continuous implies F | H is semi-continuous ) :: thesis: ( ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

proof

( F | H is onto implies F is onto )
assume A4:
F is semi-continuous
; :: thesis: F | H is semi-continuous

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;

end;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: for e, v, w being object st e in dom g & v in dom f & w in dom f & g . e Joins f . v,f . w,G2 holds

e Joins v,w,H

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

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

assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( g . e Joins f . v,f . w,G2 implies e Joins v,w,H )

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: e Joins v,w,H

then e Joins v,w,G1 by A4, A5, A6;

hence e Joins v,w,H by A5, GLIB_000:73; :: thesis: verum

end;assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( g . e Joins f . v,f . w,G2 implies e Joins v,w,H )

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: e Joins v,w,H

then e Joins v,w,G1 by A4, A5, A6;

hence e Joins v,w,H by A5, GLIB_000:73; :: thesis: verum

proof

hence
( not F is onto implies not F | H is onto )
; :: thesis: ( ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )
assume
F | H is onto
; :: thesis: F is onto

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: verum

end;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: verum

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

proof

thus
( F is semi-Dcontinuous implies F | H is semi-Dcontinuous )
:: thesis: verum
assume A7:
F is directed
; :: thesis: F | H is directed

let e, v, w be object ; :: according to GLIB_010:def 14 :: thesis: ( e in dom ((F | H) _E) & v in dom ((F | H) _V) & w in dom ((F | H) _V) & e DJoins v,w,H implies ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2 )

assume ( e in dom ((F | H) _E) & v in dom ((F | H) _V) & w in dom ((F | H) _V) ) ; :: thesis: ( not e DJoins v,w,H or ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2 )

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: ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2

( 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: verum

end;let e, v, w be object ; :: according to GLIB_010:def 14 :: thesis: ( e in dom ((F | H) _E) & v in dom ((F | H) _V) & w in dom ((F | H) _V) & e DJoins v,w,H implies ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2 )

assume ( e in dom ((F | H) _E) & v in dom ((F | H) _V) & w in dom ((F | H) _V) ) ; :: thesis: ( not e DJoins v,w,H or ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2 )

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: ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2

( 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: verum

proof

assume A11:
F is semi-Dcontinuous
; :: thesis: F | H is semi-Dcontinuous

let e, v, w be object ; :: according to GLIB_010:def 17 :: thesis: ( e in dom ((F | H) _E) & v in dom ((F | H) _V) & w in dom ((F | H) _V) & ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2 implies e DJoins v,w,H )

assume ( e in dom ((F | H) _E) & v in dom ((F | H) _V) & w in dom ((F | H) _V) ) ; :: thesis: ( not ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2 or e DJoins v,w,H )

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: e DJoins v,w,H

then e DJoins v,w,G1 by A11, A12, A13;

hence e DJoins v,w,H by A12, GLIB_000:73; :: thesis: verum

end;let e, v, w be object ; :: according to GLIB_010:def 17 :: thesis: ( e in dom ((F | H) _E) & v in dom ((F | H) _V) & w in dom ((F | H) _V) & ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2 implies e DJoins v,w,H )

assume ( e in dom ((F | H) _E) & v in dom ((F | H) _V) & w in dom ((F | H) _V) ) ; :: thesis: ( not ((F | H) _E) . e DJoins ((F | H) _V) . v,((F | H) _V) . w,G2 or e DJoins v,w,H )

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: e DJoins v,w,H

then e DJoins v,w,G1 by A11, A12, A13;

hence e DJoins v,w,H by A12, GLIB_000:73; :: thesis: verum