let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is onto holds
rng (SG2SGFunc F) = G2 .allSG()
let F be PGraphMapping of G1,G2; :: thesis: ( F is onto implies rng (SG2SGFunc F) = G2 .allSG() )
assume A1: F is onto ; :: thesis: rng (SG2SGFunc F) = G2 .allSG()

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

let x be object ; :: thesis: ( x in G2 .allSG() implies x in rng (SG2SGFunc F) )
assume x in G2 .allSG() ; :: thesis: x in rng (SG2SGFunc F)
then reconsider H2 = x as plain Subgraph of G2 by Th1;
set H1 = the plain inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2);
the plain inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) in G1 .allSG() by Th1;
then A2: the plain inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) in dom (SG2SGFunc F) by FUNCT_2:def 1;
rng F == G2 by A1, GLIB_010:56;
then H2 is Subgraph of rng F by GLIB_000:91;
then H2 = rng (F | the plain inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2)) by A1, GLIB_009:44, GLIBPRE1:99
.= (SG2SGFunc F) . the plain inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) by Def5 ;
hence x in rng (SG2SGFunc F) by A2, FUNCT_1:def 3; :: thesis: verum

end;

then G2 .allSG() c= rng (SG2SGFunc F) by TARSKI:def 3;
hence rng (SG2SGFunc F) = G2 .allSG() by XBOOLE_0:def 10; :: thesis: verum