let G1, G2 be _Graph; :: thesis: for H being Subgraph of G2
for F being PGraphMapping of G1,G2 holds
( ( F is empty implies H |` F is empty ) & ( F is one-to-one implies H |` F is one-to-one ) & ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
let H be Subgraph of G2; :: thesis: for F being PGraphMapping of G1,G2 holds
( ( F is empty implies H |` F is empty ) & ( F is one-to-one implies H |` F is one-to-one ) & ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
let F be PGraphMapping of G1,G2; :: thesis: ( ( F is empty implies H |` F is empty ) & ( F is one-to-one implies H |` F is one-to-one ) & ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
reconsider f = (the_Vertices_of H) |` (F _V) as PartFunc of (the_Vertices_of G1),(the_Vertices_of H) by PARTFUN1:12;
reconsider g = (the_Edges_of H) |` (F _E) as PartFunc of (the_Edges_of G1),(the_Edges_of H) by PARTFUN1:12;

hereby :: thesis: ( ( F is one-to-one implies H |` F is one-to-one ) & ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )

assume F is empty ; :: thesis: H |` F is empty
then F _V is empty ;
hence H |` F is empty by RELAT_1:86, XBOOLE_1:3; :: thesis: verum

end;

thus ( F is one-to-one implies H |` F is one-to-one ) by FUNCT_1:58; :: thesis: ( ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
thus ( F is onto implies H |` F is onto ) :: thesis: ( ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )

proof

assume A1: F is onto ; :: thesis: H |` F is onto
thus rng ((H |` F) _V) = (rng (F _V)) /\ (the_Vertices_of H) by RELAT_1:88
.= the_Vertices_of H by A1, XBOOLE_1:28 ; :: according to GLIB_010:def 12 :: thesis: rng ((H |` F) _E) = the_Edges_of H
thus rng ((H |` F) _E) = (rng (F _E)) /\ (the_Edges_of H) by RELAT_1:88
.= the_Edges_of H by A1, XBOOLE_1:28 ; :: thesis: verum

end;

now :: thesis: ( H |` F is total implies ( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 ) )

assume A2: H |` F is total ; :: thesis: ( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 )
dom ((H |` F) _V) c= dom (F _V) by RELAT_1:186;
hence dom (F _V) = the_Vertices_of G1 by A2, XBOOLE_0:def 10; :: thesis: dom (F _E) = the_Edges_of G1
dom ((H |` F) _E) c= dom (F _E) by RELAT_1:186;
hence dom (F _E) = the_Edges_of G1 by A2, XBOOLE_0:def 10; :: thesis: verum

end;

hence ( not F is total implies not H |` F is total ) ; :: thesis: ( ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
thus ( F is directed implies H |` F is directed ) :: thesis: ( ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )

proof

assume A3: F is directed ; :: thesis: H |` F is directed
let e, v, w be object ; :: according to GLIB_010:def 14 :: thesis: ( e in dom ((H |` F) _E) & v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e DJoins v,w,G1 implies ((H |` F) _E) . e DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H )
assume A4: ( e in dom ((H |` F) _E) & v in dom ((H |` F) _V) & w in dom ((H |` F) _V) ) ; :: thesis: ( not e DJoins v,w,G1 or ((H |` F) _E) . e DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H )
then A5: ( e in dom (F _E) & (F _E) . e in the_Edges_of H & v in dom (F _V) & (F _V) . v in the_Vertices_of H & w in dom (F _V) & (F _V) . w in the_Vertices_of H ) by FUNCT_1:54;
then ( e DJoins v,w,G1 implies (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ) by A3;
then A6: ( e DJoins v,w,G1 implies (F _E) . e DJoins (F _V) . v,(F _V) . w,H ) by A5, GLIB_000:73;
( ((H |` F) _E) . e = (F _E) . e & ((H |` F) _V) . v = (F _V) . v & ((H |` F) _V) . w = (F _V) . w ) by A4, FUNCT_1:53;
hence ( e DJoins v,w,G1 implies ((H |` F) _E) . e DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H ) by A6; :: thesis: verum

end;

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

proof

assume A7: F is semi-continuous ; :: thesis: H |` F is semi-continuous
reconsider f = (the_Vertices_of H) |` (F _V) as PartFunc of (the_Vertices_of G1),(the_Vertices_of H) by PARTFUN1:12;
reconsider g = (the_Edges_of H) |` (F _E) as PartFunc of (the_Edges_of G1),(the_Edges_of H) by PARTFUN1:12;
let e, v, w be object ; :: according to GLIB_010:def 15 :: thesis: ( e in dom ((H |` F) _E) & v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & ((H |` F) _E) . e Joins ((H |` F) _V) . v,((H |` F) _V) . w,H implies e Joins v,w,G1 )
assume A8: ( e in dom ((H |` F) _E) & v in dom ((H |` F) _V) & w in dom ((H |` F) _V) ) ; :: thesis: ( not ((H |` F) _E) . e Joins ((H |` F) _V) . v,((H |` F) _V) . w,H or e Joins v,w,G1 )
then ( e in dom (F _E) & (F _E) . e in the_Edges_of H & v in dom (F _V) & (F _V) . v in the_Vertices_of H & w in dom (F _V) & (F _V) . w in the_Vertices_of H ) by FUNCT_1:54;
then ( (F _E) . e Joins (F _V) . v,(F _V) . w,G2 implies e Joins v,w,G1 ) by A7;
then A9: ( (F _E) . e Joins (F _V) . v,(F _V) . w,H implies e Joins v,w,G1 ) by GLIB_000:72;
( g . e = (F _E) . e & f . v = (F _V) . v & f . w = (F _V) . w ) by A8, FUNCT_1:53;
hence ( not ((H |` F) _E) . e Joins ((H |` F) _V) . v,((H |` F) _V) . w,H or e Joins v,w,G1 ) by A9; :: thesis: verum

end;

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

proof

assume A10: F is continuous ; :: thesis: H |` F is continuous

now :: thesis: for e9, v, w being object st v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e9 Joins ((H |` F) _V) . v,((H |` F) _V) . w,H holds
ex e being object st
( e Joins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )

let e9, v, w be object ; :: thesis: ( v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e9 Joins ((H |` F) _V) . v,((H |` F) _V) . w,H implies ex e being object st
( e Joins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 ) )
set f = (the_Vertices_of H) |` (F _V);
assume A11: ( v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e9 Joins ((H |` F) _V) . v,((H |` F) _V) . w,H ) ; :: thesis: ex e being object st
( e Joins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )
then A12: ( v in dom ((the_Vertices_of H) |` (F _V)) & w in dom ((the_Vertices_of H) |` (F _V)) & e9 Joins ((the_Vertices_of H) |` (F _V)) . v,((the_Vertices_of H) |` (F _V)) . w,H ) ;
then A13: ( ((the_Vertices_of H) |` (F _V)) . v = (F _V) . v & ((the_Vertices_of H) |` (F _V)) . w = (F _V) . w ) by FUNCT_1:55;
A14: ( v in dom (F _V) & (F _V) . v in the_Vertices_of H & w in dom (F _V) & (F _V) . w in the_Vertices_of H & v is set & w is set ) by A11, FUNCT_1:54;
e9 Joins (F _V) . v,(F _V) . w,G2 by A12, A13, GLIB_000:72;
then consider e being object such that
A15: ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A10, A14;
take e = e; :: thesis: ( e Joins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )
thus e Joins v,w,G1 by A15; :: thesis: ( e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )
e9 in the_Edges_of H by A11, GLIB_000:def 13;
then e in dom ((the_Edges_of H) |` (F _E)) by A15, FUNCT_1:54;
hence ( e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 ) by A15, FUNCT_1:55; :: thesis: verum

end;

hence H |` F is continuous ; :: thesis: verum

end;

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

proof

assume A16: F is semi-Dcontinuous ; :: thesis: H |` F is semi-Dcontinuous
let e, v, w be object ; :: according to GLIB_010:def 17 :: thesis: ( e in dom ((H |` F) _E) & v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & ((H |` F) _E) . e DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H implies e DJoins v,w,G1 )
assume A17: ( e in dom ((H |` F) _E) & v in dom ((H |` F) _V) & w in dom ((H |` F) _V) ) ; :: thesis: ( not ((H |` F) _E) . e DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H or e DJoins v,w,G1 )
then ( e in dom (F _E) & (F _E) . e in the_Edges_of H & v in dom (F _V) & (F _V) . v in the_Vertices_of H & w in dom (F _V) & (F _V) . w in the_Vertices_of H ) by FUNCT_1:54;
then A18: ( (F _E) . e DJoins (F _V) . v,(F _V) . w,H implies e DJoins v,w,G1 ) by A16, GLIB_000:72;
( ((H |` F) _E) . e = (F _E) . e & ((H |` F) _V) . v = (F _V) . v & ((H |` F) _V) . w = (F _V) . w ) by A17, FUNCT_1:53;
hence ( ((H |` F) _E) . e DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H implies e DJoins v,w,G1 ) by A18; :: thesis: verum

end;

thus ( F is Dcontinuous implies H |` F is Dcontinuous ) :: thesis: verum

proof

assume A19: F is Dcontinuous ; :: thesis: H |` F is Dcontinuous

now :: thesis: for e9, v, w being object st v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e9 DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H holds
ex e being object st
( e DJoins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )

let e9, v, w be object ; :: thesis: ( v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e9 DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H implies ex e being object st
( e DJoins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 ) )
set f = (the_Vertices_of H) |` (F _V);
assume A20: ( v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e9 DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H ) ; :: thesis: ex e being object st
( e DJoins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )
then A21: ( v in dom ((the_Vertices_of H) |` (F _V)) & w in dom ((the_Vertices_of H) |` (F _V)) & e9 DJoins ((the_Vertices_of H) |` (F _V)) . v,((the_Vertices_of H) |` (F _V)) . w,H ) ;
then A22: ( ((the_Vertices_of H) |` (F _V)) . v = (F _V) . v & ((the_Vertices_of H) |` (F _V)) . w = (F _V) . w ) by FUNCT_1:55;
A23: ( v in dom (F _V) & (F _V) . v in the_Vertices_of H & w in dom (F _V) & (F _V) . w in the_Vertices_of H & v is set & w is set ) by A20, FUNCT_1:54;
e9 DJoins (F _V) . v,(F _V) . w,G2 by A21, A22, GLIB_000:72;
then consider e being object such that
A24: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A19, A23;
take e = e; :: thesis: ( e DJoins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )
thus e DJoins v,w,G1 by A24; :: thesis: ( e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )
e9 in the_Edges_of H by A20, GLIB_000:def 14;
then e in dom ((the_Edges_of H) |` (F _E)) by A24, FUNCT_1:54;
hence ( e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 ) by A24, FUNCT_1:55; :: thesis: verum

end;

hence H |` F is Dcontinuous ; :: thesis: verum

end;