let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st rng (F _V) = the_Vertices_of G2 holds
rng ((SG2SGFunc F) | (G1 .allSpanningSG())) c= G2 .allSpanningSG()
let F be PGraphMapping of G1,G2; :: thesis: ( rng (F _V) = the_Vertices_of G2 implies rng ((SG2SGFunc F) | (G1 .allSpanningSG())) c= G2 .allSpanningSG() )
assume A1: rng (F _V) = the_Vertices_of G2 ; :: thesis: rng ((SG2SGFunc F) | (G1 .allSpanningSG())) c= G2 .allSpanningSG()
set f = (SG2SGFunc F) | (G1 .allSpanningSG());
A3: dom ((SG2SGFunc F) | (G1 .allSpanningSG())) = G1 .allSpanningSG() by FUNCT_2:def 1;

now :: thesis: for y being object st y in rng ((SG2SGFunc F) | (G1 .allSpanningSG())) holds
y in G2 .allSpanningSG()

let y be object ; :: thesis: ( y in rng ((SG2SGFunc F) | (G1 .allSpanningSG())) implies y in G2 .allSpanningSG() )
assume A4: y in rng ((SG2SGFunc F) | (G1 .allSpanningSG())) ; :: thesis: y in G2 .allSpanningSG()
then consider x being object such that
A5: ( x in dom ((SG2SGFunc F) | (G1 .allSpanningSG())) & ((SG2SGFunc F) | (G1 .allSpanningSG())) . x = y ) by FUNCT_1:def 3;
consider H1 being Element of [#] (G1 .allSG()) such that
A6: ( x = H1 & H1 is spanning ) by A3, A5;
reconsider H2 = y as Element of [#] (G2 .allSG()) by A4;
A7: (F | H1) _V = (F _V) | (the_Vertices_of G1) by A6, GLIB_000:def 33
.= F _V ;
H2 = (SG2SGFunc F) . x by A5, FUNCT_1:47
.= rng (F | H1) by A6, Def5 ;
then H2 is spanning by A1, A7;
hence y in G2 .allSpanningSG() ; :: thesis: verum

end;

hence rng ((SG2SGFunc F) | (G1 .allSpanningSG())) c= G2 .allSpanningSG() by TARSKI:def 3; :: thesis: verum