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;

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 ) )

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 ) )

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 ) )

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 ) )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;then F _V is empty ;

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

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;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

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

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 ) )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;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

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

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 ) )
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;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

proof

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 ) )
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;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

proof

thus
( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous )
:: thesis: ( F is Dcontinuous implies H |` F is Dcontinuous )
assume A10:
F is continuous
; :: thesis: H |` F is continuous

end;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 )

hence
H |` F is continuous
; :: thesis: verumex 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;( 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

proof

thus
( F is Dcontinuous implies H |` F is Dcontinuous )
:: thesis: verum
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;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

proof

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

end;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 )

hence
H |` F is Dcontinuous
; :: thesis: verumex 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;( 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