let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is total & F is continuous holds
rng ((SG2SGFunc F) | (G1 .allInducedSG())) c= G2 .allInducedSG()
let F be PGraphMapping of G1,G2; :: thesis: ( F is total & F is continuous implies rng ((SG2SGFunc F) | (G1 .allInducedSG())) c= G2 .allInducedSG() )
assume A1: ( F is total & F is continuous ) ; :: thesis: rng ((SG2SGFunc F) | (G1 .allInducedSG())) c= G2 .allInducedSG()
set f = (SG2SGFunc F) | (G1 .allInducedSG());
A2: dom ((SG2SGFunc F) | (G1 .allInducedSG())) = G1 .allInducedSG() by FUNCT_2:def 1;

now :: thesis: for x being object st x in rng ((SG2SGFunc F) | (G1 .allInducedSG())) holds
x in G2 .allInducedSG()

let x be object ; :: thesis: ( x in rng ((SG2SGFunc F) | (G1 .allInducedSG())) implies x in G2 .allInducedSG() )
assume x in rng ((SG2SGFunc F) | (G1 .allInducedSG())) ; :: thesis: x in G2 .allInducedSG()
then consider y being object such that
A3: ( y in dom ((SG2SGFunc F) | (G1 .allInducedSG())) & x = ((SG2SGFunc F) | (G1 .allInducedSG())) . y ) by FUNCT_1:def 3;
consider V1 being non empty Subset of (the_Vertices_of G1) such that
A4: y = the plain inducedSubgraph of G1,V1 by A2, A3;
reconsider H1 = y as inducedSubgraph of G1,V1 by A4;
dom (F _V) = the_Vertices_of G1 by A1, GLIB_010:def 11;
then A5: (F _V) .: V1 is non empty Subset of (the_Vertices_of G2) by RELAT_1:119;
G1 == dom F by A1, GLIB_010:55;
then A6: the_Vertices_of G1 = the_Vertices_of (dom F) by GLIB_000:def 34;
x = (SG2SGFunc F) . y by A3, FUNCT_1:47
.= rng (F | H1) by A4, Def5 ;
then x is plain inducedSubgraph of G2,((F _V) .: V1) by A1, A6, GLIBPRE1:102;
hence x in G2 .allInducedSG() by A5, Th45; :: thesis: verum

end;

hence rng ((SG2SGFunc F) | (G1 .allInducedSG())) c= G2 .allInducedSG() by TARSKI:def 3; :: thesis: verum