let G1, G2 be _Graph; :: thesis: for V being set

for H being inducedSubgraph of G1,V

for F being PGraphMapping of G1,G2 holds

( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

let V be set ; :: thesis: for H being inducedSubgraph of G1,V

for F being PGraphMapping of G1,G2 holds

( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

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

( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

let F be PGraphMapping of G1,G2; :: thesis: ( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

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;

for H being inducedSubgraph of G1,V

for F being PGraphMapping of G1,G2 holds

( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

let V be set ; :: thesis: for H being inducedSubgraph of G1,V

for F being PGraphMapping of G1,G2 holds

( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

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

( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

let F be PGraphMapping of G1,G2; :: thesis: ( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

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;

per cases
( V is non empty Subset of (the_Vertices_of G1) or not V is non empty Subset of (the_Vertices_of G1) )
;

end;

suppose
V is non empty Subset of (the_Vertices_of G1)
; :: thesis: ( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

then A1:
( the_Vertices_of H = V & the_Edges_of H = G1 .edgesBetween V )
by GLIB_000:def 37;

end;hereby :: thesis: ( ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

hence
( F is strong_SG-embedding implies F | H is strong_SG-embedding )
by Th57; :: thesis: ( F is Dcontinuous implies F | H is Dcontinuous )assume A2:
F is continuous
; :: thesis: F | H is continuous

end;now :: thesis: for e9, v, w being object st v in dom f & w in dom f & e9 Joins f . v,f . w,G2 holds

ex e being object st

( e Joins v,w,H & e in dom g & g . e = e9 )

hence
F | H is continuous
; :: thesis: verumex e being object st

( e Joins v,w,H & e in dom g & g . e = e9 )

let e9, v, w be object ; :: thesis: ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 implies ex e being object st

( e Joins v,w,H & e in dom g & g . e = e9 ) )

assume A3: ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 ) ; :: thesis: ex e being object st

( e Joins v,w,H & e in dom g & g . e = e9 )

then A4: ( v in dom (F _V) & v in the_Vertices_of H & w in dom (F _V) & w in the_Vertices_of H & v is set & w is set ) by RELAT_1:57;

then ( f . v = (F _V) . v & f . w = (F _V) . w ) by FUNCT_1:49;

then consider e being object such that

A5: ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A2, A3, A4;

take e = e; :: thesis: ( e Joins v,w,H & e in dom g & g . e = e9 )

e in G1 .edgesBetween V by A1, A4, A5, GLIB_000:32;

then A6: e in the_Edges_of H by A1;

hence e Joins v,w,H by A4, A5, GLIB_000:73; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A5, A6, RELAT_1:57, FUNCT_1:49; :: thesis: verum

end;( e Joins v,w,H & e in dom g & g . e = e9 ) )

assume A3: ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 ) ; :: thesis: ex e being object st

( e Joins v,w,H & e in dom g & g . e = e9 )

then A4: ( v in dom (F _V) & v in the_Vertices_of H & w in dom (F _V) & w in the_Vertices_of H & v is set & w is set ) by RELAT_1:57;

then ( f . v = (F _V) . v & f . w = (F _V) . w ) by FUNCT_1:49;

then consider e being object such that

A5: ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A2, A3, A4;

take e = e; :: thesis: ( e Joins v,w,H & e in dom g & g . e = e9 )

e in G1 .edgesBetween V by A1, A4, A5, GLIB_000:32;

then A6: e in the_Edges_of H by A1;

hence e Joins v,w,H by A4, A5, GLIB_000:73; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A5, A6, RELAT_1:57, FUNCT_1:49; :: thesis: verum

hereby :: thesis: verum

assume A7:
F is Dcontinuous
; :: thesis: F | H is Dcontinuous

end;now :: thesis: for e9, v, w being object st v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 holds

ex e being object st

( e DJoins v,w,H & e in dom g & g . e = e9 )

hence
F | H is Dcontinuous
; :: thesis: verumex e being object st

( e DJoins v,w,H & e in dom g & g . e = e9 )

let e9, v, w be object ; :: thesis: ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 implies ex e being object st

( e DJoins v,w,H & e in dom g & g . e = e9 ) )

assume A8: ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 ) ; :: thesis: ex e being object st

( e DJoins v,w,H & e in dom g & g . e = e9 )

then A9: ( v in dom (F _V) & v in the_Vertices_of H & w in dom (F _V) & w in the_Vertices_of H & v is set & w is set ) by RELAT_1:57;

then ( f . v = (F _V) . v & f . w = (F _V) . w ) by FUNCT_1:49;

then consider e being object such that

A10: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A7, A8, A9;

take e = e; :: thesis: ( e DJoins v,w,H & e in dom g & g . e = e9 )

e Joins v,w,G1 by A10, GLIB_000:16;

then e in G1 .edgesBetween V by A1, A9, GLIB_000:32;

then A11: e in the_Edges_of H by A1;

hence e DJoins v,w,H by A9, A10, GLIB_000:73; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A10, A11, RELAT_1:57, FUNCT_1:49; :: thesis: verum

end;( e DJoins v,w,H & e in dom g & g . e = e9 ) )

assume A8: ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 ) ; :: thesis: ex e being object st

( e DJoins v,w,H & e in dom g & g . e = e9 )

then A9: ( v in dom (F _V) & v in the_Vertices_of H & w in dom (F _V) & w in the_Vertices_of H & v is set & w is set ) by RELAT_1:57;

then ( f . v = (F _V) . v & f . w = (F _V) . w ) by FUNCT_1:49;

then consider e being object such that

A10: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A7, A8, A9;

take e = e; :: thesis: ( e DJoins v,w,H & e in dom g & g . e = e9 )

e Joins v,w,G1 by A10, GLIB_000:16;

then e in G1 .edgesBetween V by A1, A9, GLIB_000:32;

then A11: e in the_Edges_of H by A1;

hence e DJoins v,w,H by A9, A10, GLIB_000:73; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A10, A11, RELAT_1:57, FUNCT_1:49; :: thesis: verum

suppose
V is not non empty Subset of (the_Vertices_of G1)
; :: thesis: ( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

then A12:
G1 == H
by GLIB_000:def 37;

then ( the_Vertices_of G1 = the_Vertices_of H & the_Edges_of G1 = the_Edges_of H ) by GLIB_000:def 34;

then A13: ( f = F _V & g = F _E ) ;

end;then ( the_Vertices_of G1 = the_Vertices_of H & the_Edges_of G1 = the_Edges_of H ) by GLIB_000:def 34;

then A13: ( f = F _V & g = F _E ) ;

hereby :: thesis: ( ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

hence
( F is strong_SG-embedding implies F | H is strong_SG-embedding )
by Th57; :: thesis: ( F is Dcontinuous implies F | H is Dcontinuous )assume A14:
F is continuous
; :: thesis: F | H is continuous

end;now :: thesis: for e9, v, w being object st v in dom f & w in dom f & e9 Joins f . v,f . w,G2 holds

ex e being object st

( e Joins v,w,H & e in dom g & g . e = e9 )

hence
F | H is continuous
; :: thesis: verumex e being object st

( e Joins v,w,H & e in dom g & g . e = e9 )

let e9, v, w be object ; :: thesis: ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 implies ex e being object st

( e Joins v,w,H & e in dom g & g . e = e9 ) )

assume ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 ) ; :: thesis: ex e being object st

( e Joins v,w,H & e in dom g & g . e = e9 )

then consider e being object such that

A15: ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A13, A14;

take e = e; :: thesis: ( e Joins v,w,H & e in dom g & g . e = e9 )

thus e Joins v,w,H by A12, A15, GLIB_000:88; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A13, A15; :: thesis: verum

end;( e Joins v,w,H & e in dom g & g . e = e9 ) )

assume ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 ) ; :: thesis: ex e being object st

( e Joins v,w,H & e in dom g & g . e = e9 )

then consider e being object such that

A15: ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A13, A14;

take e = e; :: thesis: ( e Joins v,w,H & e in dom g & g . e = e9 )

thus e Joins v,w,H by A12, A15, GLIB_000:88; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A13, A15; :: thesis: verum

hereby :: thesis: verum

assume A16:
F is Dcontinuous
; :: thesis: F | H is Dcontinuous

end;now :: thesis: for e9, v, w being object st v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 holds

ex e being object st

( e DJoins v,w,H & e in dom g & g . e = e9 )

hence
F | H is Dcontinuous
; :: thesis: verumex e being object st

( e DJoins v,w,H & e in dom g & g . e = e9 )

let e9, v, w be object ; :: thesis: ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 implies ex e being object st

( e DJoins v,w,H & e in dom g & g . e = e9 ) )

assume ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 ) ; :: thesis: ex e being object st

( e DJoins v,w,H & e in dom g & g . e = e9 )

then consider e being object such that

A17: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A13, A16;

take e = e; :: thesis: ( e DJoins v,w,H & e in dom g & g . e = e9 )

thus e DJoins v,w,H by A12, A17, GLIB_000:88; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A13, A17; :: thesis: verum

end;( e DJoins v,w,H & e in dom g & g . e = e9 ) )

assume ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 ) ; :: thesis: ex e being object st

( e DJoins v,w,H & e in dom g & g . e = e9 )

then consider e being object such that

A17: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A13, A16;

take e = e; :: thesis: ( e DJoins v,w,H & e in dom g & g . e = e9 )

thus e DJoins v,w,H by A12, A17, GLIB_000:88; :: thesis: ( e in dom g & g . e = e9 )

thus ( e in dom g & g . e = e9 ) by A13, A17; :: thesis: verum