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