let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & F is onto holds
G2 .allSpanningForests() = rng ((SG2SGFunc F) | (G1 .allSpanningForests()))
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding & F is onto implies G2 .allSpanningForests() = rng ((SG2SGFunc F) | (G1 .allSpanningForests())) )
set f = SG2SGFunc F;
assume A1: ( F is weak_SG-embedding & F is onto ) ; :: thesis: G2 .allSpanningForests() = rng ((SG2SGFunc F) | (G1 .allSpanningForests()))
then rng (F _V) = the_Vertices_of G2 by GLIB_010:def 12;
then A2: rng ((SG2SGFunc F) | (G1 .allSpanningForests())) c= G2 .allSpanningForests() by A1, Th113;
dom (F _V) = the_Vertices_of G1 by A1, GLIB_010:def 11;
then F _V is total by PARTFUN1:def 2;
then ( G2 .allForests() c= rng ((SG2SGFunc F) | (G1 .allForests())) & G2 .allSpanningSG() c= rng ((SG2SGFunc F) | (G1 .allSpanningSG())) ) by A1, Th68, Th91;
then (G2 .allForests()) /\ (G2 .allSpanningSG()) c= (rng ((SG2SGFunc F) | (G1 .allForests()))) /\ (rng ((SG2SGFunc F) | (G1 .allSpanningSG()))) by XBOOLE_1:27;
then A3: G2 .allSpanningForests() c= (rng ((SG2SGFunc F) | (G1 .allForests()))) /\ (rng ((SG2SGFunc F) | (G1 .allSpanningSG()))) by Th103;
A4: rng ((SG2SGFunc F) | (G1 .allForests())) = (SG2SGFunc F) .: (G1 .allForests()) by RELAT_1:115;
A5: rng ((SG2SGFunc F) | (G1 .allSpanningSG())) = (SG2SGFunc F) .: (G1 .allSpanningSG()) by RELAT_1:115;
A6: SG2SGFunc F is one-to-one by A1, Th31;
(rng ((SG2SGFunc F) | (G1 .allForests()))) /\ (rng ((SG2SGFunc F) | (G1 .allSpanningSG()))) = (SG2SGFunc F) .: ((G1 .allForests()) /\ (G1 .allSpanningSG())) by A4, A5, A6, FUNCT_1:62
.= rng ((SG2SGFunc F) | ((G1 .allForests()) /\ (G1 .allSpanningSG()))) by RELAT_1:115
.= rng ((SG2SGFunc F) | (G1 .allSpanningForests())) by Th103 ;
hence G2 .allSpanningForests() = rng ((SG2SGFunc F) | (G1 .allSpanningForests())) by A2, A3, XBOOLE_0:def 10; :: thesis: verum