let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is onto & F _V is one-to-one & F _V is total holds
rng ((SG2SGFunc F) | (G1 .allSpanningSG())) = G2 .allSpanningSG()
let F be PGraphMapping of G1,G2; :: thesis: ( F is onto & F _V is one-to-one & F _V is total implies rng ((SG2SGFunc F) | (G1 .allSpanningSG())) = G2 .allSpanningSG() )
set f = (SG2SGFunc F) | (G1 .allSpanningSG());
assume A1: ( F is onto & F _V is one-to-one & F _V is total ) ; :: thesis: rng ((SG2SGFunc F) | (G1 .allSpanningSG())) = G2 .allSpanningSG()
then rng (F _V) = the_Vertices_of G2 by GLIB_010:def 12;
then A2: rng ((SG2SGFunc F) | (G1 .allSpanningSG())) c= G2 .allSpanningSG() by Th67;

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

let y be object ; :: thesis: ( y in G2 .allSpanningSG() implies y in rng ((SG2SGFunc F) | (G1 .allSpanningSG())) )
assume y in G2 .allSpanningSG() ; :: thesis: y in rng ((SG2SGFunc F) | (G1 .allSpanningSG()))
then consider H2 being Element of [#] (G2 .allSG()) such that
A3: ( y = H2 & H2 is spanning ) ;
H2 in G2 .allSG() ;
then H2 in rng (SG2SGFunc F) by A1, Th32;
then consider x being object such that
A4: ( x in dom (SG2SGFunc F) & (SG2SGFunc F) . x = H2 ) by FUNCT_1:def 3;
reconsider H1 = x as plain Subgraph of G1 by A4, Th1;
dom (F _V) = the_Vertices_of G1 by A1, PARTFUN1:def 2;
then A5: the_Vertices_of H1 c= dom (F _V) ;
then dom ((F | H1) _V) <> {} by RELAT_1:62;
then A6: not F | H1 is empty ;
A7: H2 = rng (F | H1) by A4, Def5;
the_Vertices_of H1 = (F _V) " ((F _V) .: (the_Vertices_of H1)) by A1, A5, FUNCT_1:94
.= (F _V) " (rng ((F _V) | (the_Vertices_of H1))) by RELAT_1:115
.= (F _V) " (the_Vertices_of (rng (F | H1))) by A6, GLIB_010:54
.= (F _V) " (the_Vertices_of G2) by A3, A7, GLIB_000:def 33
.= dom (F _V) by RELSET_1:22
.= the_Vertices_of G1 by A1, PARTFUN1:def 2 ;
then H1 is spanning by GLIB_000:def 33;
then A8: x in dom ((SG2SGFunc F) | (G1 .allSpanningSG())) by A4, Th60, RELAT_1:57;
then H2 = ((SG2SGFunc F) | (G1 .allSpanningSG())) . x by A4, FUNCT_1:47;
hence y in rng ((SG2SGFunc F) | (G1 .allSpanningSG())) by A3, A8, FUNCT_1:3; :: thesis: verum

end;

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