let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is total holds
(rng F) |` F is total
let F be PGraphMapping of G1,G2; :: thesis: ( F is total implies (rng F) |` F is total )
assume A1: F is total ; :: thesis: (rng F) |` F is total
A2: dom (((rng F) |` F) _V) = dom (F _V) by Th86
.= the_Vertices_of G1 by A1, GLIB_010:def 11 ;
dom (((rng F) |` F) _E) = dom (F _E) by Th86
.= the_Edges_of G1 by A1, GLIB_010:def 11 ;
hence (rng F) |` F is total by A2, GLIB_010:def 11; :: thesis: verum