let G1, G2 be non-multi _Graph; for f being PVertexMapping of G1,G2 st f is onto & f is continuous holds
PVM2PGM f is onto
let f be PVertexMapping of G1,G2; ( f is onto & f is continuous implies PVM2PGM f is onto )
assume A1:
( f is onto & f is continuous )
; PVM2PGM f is onto
then A2:
rng ((PVM2PGM f) _V) = the_Vertices_of G2
by FUNCT_2:def 3;
set g = (PVM2PGM f) _E ;
for e being object st e in the_Edges_of G2 holds
e in rng ((PVM2PGM f) _E)
proof
let e be
object ;
( e in the_Edges_of G2 implies e in rng ((PVM2PGM f) _E) )
set v2 =
(the_Source_of G2) . e;
set w2 =
(the_Target_of G2) . e;
assume
e in the_Edges_of G2
;
e in rng ((PVM2PGM f) _E)
then
e in G2 .edgesBetween (the_Vertices_of G2)
by GLIB_000:34;
then
e in G2 .edgesBetween (rng f)
by A1, FUNCT_2:def 3;
then A3:
(
e in the_Edges_of G2 &
(the_Source_of G2) . e in rng f &
(the_Target_of G2) . e in rng f )
by GLIB_000:31;
consider v1 being
object such that A4:
(
v1 in dom f &
f . v1 = (the_Source_of G2) . e )
by A3, FUNCT_1:def 3;
consider w1 being
object such that A5:
(
w1 in dom f &
f . w1 = (the_Target_of G2) . e )
by A3, FUNCT_1:def 3;
A6:
e Joins f . v1,
f . w1,
G2
by A3, A4, A5, GLIB_000:def 13;
then consider e0 being
object such that A7:
e0 Joins v1,
w1,
G1
by A1, A4, A5, Th2;
e0 in G1 .edgesBetween (dom f)
by A4, A5, A7, GLIB_000:32;
then A8:
e0 in dom ((PVM2PGM f) _E)
by Def10;
then
((PVM2PGM f) _E) . e0 Joins ((PVM2PGM f) _V) . v1,
((PVM2PGM f) _V) . w1,
G2
by A4, A5, A7, GLIB_010:4;
then
((PVM2PGM f) _E) . e0 = e
by A6, GLIB_000:def 20;
hence
e in rng ((PVM2PGM f) _E)
by A8, FUNCT_1:def 3;
verum
end;
then
the_Edges_of G2 c= rng ((PVM2PGM f) _E)
by TARSKI:def 3;
then
rng ((PVM2PGM f) _E) = the_Edges_of G2
by XBOOLE_0:def 10;
hence
PVM2PGM f is onto
by A2, GLIB_010:def 12; verum