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