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

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