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