let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
G2 .allConnectedSG() = rng ((SG2SGFunc F) | (G1 .allConnectedSG()))
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies G2 .allConnectedSG() = rng ((SG2SGFunc F) | (G1 .allConnectedSG())) )
assume F is isomorphism ; :: thesis: G2 .allConnectedSG() = rng ((SG2SGFunc F) | (G1 .allConnectedSG()))
then ( rng ((SG2SGFunc F) | (G1 .allConnectedSG())) c= G2 .allConnectedSG() & G2 .allConnectedSG() c= rng ((SG2SGFunc F) | (G1 .allConnectedSG())) ) by Th132, Th133;
hence G2 .allConnectedSG() = rng ((SG2SGFunc F) | (G1 .allConnectedSG())) by XBOOLE_0:def 10; :: thesis: verum