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

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

let x be object ; :: thesis: ( x in G2 .allForests() implies x in rng ((SG2SGFunc F) | (G1 .allForests())) )
assume x in G2 .allForests() ; :: thesis: x in rng ((SG2SGFunc F) | (G1 .allForests()))
then reconsider H2 = x as acyclic plain Subgraph of G2 by Th78;
rng F == G2 by A1, GLIB_010:56;
then A3: H2 is Subgraph of rng F by GLIB_000:91;
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) is acyclic by A1, A3, GLIBPRE1:107;
then A4: the plain inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) in dom ((SG2SGFunc F) | (G1 .allForests())) by A2, Th78;
A5: rng (F | the plain inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2)) = H2 by A1, A3, GLIB_009:44, GLIBPRE1:99;
((SG2SGFunc F) | (G1 .allForests())) . the plain inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) = (SG2SGFunc F) . the plain inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) by A4, FUNCT_1:47
.= H2 by A5, Def5 ;
hence x in rng ((SG2SGFunc F) | (G1 .allForests())) by A4, FUNCT_1:3; :: thesis: verum

end;

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