let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
rng ((SG2SGFunc F) | (G1 .allSpanningSG())) = G2 .allSpanningSG()
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies rng ((SG2SGFunc F) | (G1 .allSpanningSG())) = G2 .allSpanningSG() )
assume F is isomorphism ; :: thesis: rng ((SG2SGFunc F) | (G1 .allSpanningSG())) = G2 .allSpanningSG()
then ( F is onto & F _V is one-to-one & dom (F _V) = the_Vertices_of G1 ) by GLIB_010:def 11;
then ( F is onto & F _V is one-to-one & F _V is total ) by PARTFUN1:def 2;
hence rng ((SG2SGFunc F) | (G1 .allSpanningSG())) = G2 .allSpanningSG() by Th68; :: thesis: verum