let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is total holds
for v being Vertex of G1 holds (F _V) . v is Vertex of G2
let F be PGraphMapping of G1,G2; :: thesis: ( F is total implies for v being Vertex of G1 holds (F _V) . v is Vertex of G2 )
assume A1: F is total ; :: thesis: for v being Vertex of G1 holds (F _V) . v is Vertex of G2
let v be Vertex of G1; :: thesis: (F _V) . v is Vertex of G2
(F _V) . v in rng (F _V) by A1, FUNCT_1:3;
hence (F _V) . v is Vertex of G2 ; :: thesis: verum