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;

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

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;

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

assume A2: F is continuous ; :: thesis: F | H is continuous

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 )

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;

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

end;

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

hereby :: thesis: verum

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

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 )

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;

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

end;

end;

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

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

assume A14: F is continuous ; :: thesis: F | H is continuous

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 )

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;

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

end;

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

hereby :: thesis: verum

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

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 )

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;

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

end;

end;

end;