let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
rng ((SG2SGFunc F) | (G1 .allForests())) c= G2 .allForests()
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding implies rng ((SG2SGFunc F) | (G1 .allForests())) c= G2 .allForests() )
assume A1: F is weak_SG-embedding ; :: thesis: rng ((SG2SGFunc F) | (G1 .allForests())) c= G2 .allForests()
set f = (SG2SGFunc F) | (G1 .allForests());

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

let y be object ; :: thesis: ( y in rng ((SG2SGFunc F) | (G1 .allForests())) implies y in G2 .allForests() )
assume A2: y in rng ((SG2SGFunc F) | (G1 .allForests())) ; :: thesis: y in G2 .allForests()
then consider x being object such that
A3: ( x in dom ((SG2SGFunc F) | (G1 .allForests())) & ((SG2SGFunc F) | (G1 .allForests())) . x = y ) by FUNCT_1:def 3;
reconsider H1 = x as acyclic plain Subgraph of G1 by A3, Th78;
y in rng (SG2SGFunc F) by A2, TARSKI:def 3, RELAT_1:70;
then reconsider H2 = y as plain Subgraph of G2 by Th1;
A4: H2 = (SG2SGFunc F) . x by A3, FUNCT_1:47
.= rng (F | H1) by Def5 ;
H2 is acyclic

proof

assume not H2 is acyclic ; :: thesis: contradiction
then consider W2 being Walk of H2 such that
A5: W2 is Cycle-like by GLIB_002:def 2;
dom (F _V) = the_Vertices_of G1 by A1, GLIB_010:def 11;
then A6: the_Vertices_of H1 c= dom (F _V) ;
dom ((F | H1) _V) = the_Vertices_of H1 by A6, RELAT_1:62;
then reconsider F9 = F | H1 as non empty one-to-one PGraphMapping of H1,G2 by A1;
rng (F9 _V) = the_Vertices_of H2 by A4, GLIB_010:54;
then A7: W2 .vertices() c= rng (F9 _V) ;
rng (F9 _E) = the_Edges_of H2 by A4, GLIB_010:54;
then A8: W2 .edges() c= rng (F9 _E) ;
reconsider W0 = W2 as Walk of G2 by GLIB_001:167;
( W0 .edges() = W2 .edges() & W0 .vertices() = W2 .vertices() ) by GLIB_001:98, GLIB_001:110;
then reconsider W2 = W2 as F9 -valued Walk of G2 by A7, A8, GLIB_010:def 36;
W2 is Cycle-like by A5, GLIB_006:24;
then F9 " W2 is Cycle-like by GLIB_010:138;
hence contradiction by GLIB_002:def 2; :: thesis: verum

end;

hence y in G2 .allForests() by Th78; :: thesis: verum

end;

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