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 )

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

( 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 )

assume A4:
rng F == G2
; :: thesis: 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 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

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