let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2 holds
( F is onto iff rng F == G2 )
let F be non empty PGraphMapping of G1,G2; :: thesis: ( F is onto iff rng F == G2 )

hereby :: thesis: ( rng F == G2 implies F is onto )

A1: G2 is Subgraph of G2 by GLIB_000:40;
assume A2: F is onto ; :: thesis: rng F == G2
A3: the_Vertices_of (rng F) = the_Vertices_of G2 by A2, Th54;
the_Edges_of (rng F) = the_Edges_of G2 by A2, Th54;
hence rng F == G2 by A1, A3, GLIB_000:86; :: thesis: verum

end;

assume A4: rng F == G2 ; :: thesis: F is onto
A5: rng (F _V) = the_Vertices_of (rng F) by Th54
.= the_Vertices_of G2 by A4, GLIB_000:def 34 ;
rng (F _E) = the_Edges_of (rng F) by Th54
.= the_Edges_of G2 by A4, GLIB_000:def 34 ;
hence F is onto by A5; :: thesis: verum