let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & F is onto holds
G2 .allSpanningTrees() = rng ((SG2SGFunc F) | (G1 .allSpanningTrees()))
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding & F is onto implies G2 .allSpanningTrees() = rng ((SG2SGFunc F) | (G1 .allSpanningTrees())) )
set f = SG2SGFunc F;
assume A1: ( F is weak_SG-embedding & F is onto ) ; :: thesis: G2 .allSpanningTrees() = rng ((SG2SGFunc F) | (G1 .allSpanningTrees()))
then rng (F _V) = the_Vertices_of G2 by GLIB_010:def 12;
then A2: rng ((SG2SGFunc F) | (G1 .allSpanningTrees())) c= G2 .allSpanningTrees() by A1, Th179;
( G2 .allConnectedSG() c= rng ((SG2SGFunc F) | (G1 .allConnectedSG())) & G2 .allSpanningForests() c= rng ((SG2SGFunc F) | (G1 .allSpanningForests())) ) by A1, Th133, Th114;
then (G2 .allConnectedSG()) /\ (G2 .allSpanningForests()) c= (rng ((SG2SGFunc F) | (G1 .allConnectedSG()))) /\ (rng ((SG2SGFunc F) | (G1 .allSpanningForests()))) by XBOOLE_1:27;
then A3: G2 .allSpanningTrees() c= (rng ((SG2SGFunc F) | (G1 .allConnectedSG()))) /\ (rng ((SG2SGFunc F) | (G1 .allSpanningForests()))) by Th170;
A4: rng ((SG2SGFunc F) | (G1 .allConnectedSG())) = (SG2SGFunc F) .: (G1 .allConnectedSG()) by RELAT_1:115;
A5: rng ((SG2SGFunc F) | (G1 .allSpanningForests())) = (SG2SGFunc F) .: (G1 .allSpanningForests()) by RELAT_1:115;
A6: SG2SGFunc F is one-to-one by A1, Th31;
(rng ((SG2SGFunc F) | (G1 .allConnectedSG()))) /\ (rng ((SG2SGFunc F) | (G1 .allSpanningForests()))) = (SG2SGFunc F) .: ((G1 .allConnectedSG()) /\ (G1 .allSpanningForests())) by A4, A5, A6, FUNCT_1:62
.= rng ((SG2SGFunc F) | ((G1 .allConnectedSG()) /\ (G1 .allSpanningForests()))) by RELAT_1:115
.= rng ((SG2SGFunc F) | (G1 .allSpanningTrees())) by Th170 ;
hence G2 .allSpanningTrees() = rng ((SG2SGFunc F) | (G1 .allSpanningTrees())) by A2, A3, XBOOLE_0:def 10; :: thesis: verum