let G1, G2 be _Graph; :: thesis:
let V be set ; :: thesis:
let H be inducedSubgraph of G1,V; :: thesis:
let F be PGraphMapping of G1,G2; :: thesis:
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 ;

suppose V is non empty Subset of (the_Vertices_of G1) ; :: thesis:

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

hereby :: thesis:

assume A2: F is continuous ; :: thesis:

now :: thesis:

let e9, v, w be object ; :: thesis:
assume A3: ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 ) ; :: thesis:
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 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:
thus ( e in dom g & g . e = e9 ) by A5, A6, RELAT_1:57, FUNCT_1:49; :: thesis:

end;

hence F | H is continuous ; :: thesis:

end;

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

hereby :: thesis:

assume A7: F is Dcontinuous ; :: thesis:

now :: thesis:

let e9, v, w be object ; :: thesis:
assume A8: ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 ) ; :: thesis:
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 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:
thus ( e in dom g & g . e = e9 ) by A10, A11, RELAT_1:57, FUNCT_1:49; :: thesis:

end;

hence F | H is Dcontinuous ; :: thesis:

end;

end;

suppose V is not non empty Subset of (the_Vertices_of G1) ; :: thesis:

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:

assume A14: F is continuous ; :: thesis:

now :: thesis:

let e9, v, w be object ; :: thesis:
assume ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 ) ; :: thesis:
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:
thus e Joins v,w,H by A12, A15, GLIB_000:88; :: thesis:
thus ( e in dom g & g . e = e9 ) by A13, A15; :: thesis:

end;

hence F | H is continuous ; :: thesis:

end;

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

hereby :: thesis:

assume A16: F is Dcontinuous ; :: thesis:

now :: thesis:

let e9, v, w be object ; :: thesis:
assume ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 ) ; :: thesis:
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:
thus e DJoins v,w,H by A12, A17, GLIB_000:88; :: thesis:
thus ( e in dom g & g . e = e9 ) by A13, A17; :: thesis:

end;

hence F | H is Dcontinuous ; :: thesis:

end;

end;

end;