let f be VColoring of G; :: thesis: ( f is one-to-one implies f is proper )
assume A1: f is one-to-one ; :: thesis: f is proper

now :: thesis: for e, v, w being object st e Joins v,w,G holds
f . v <> f . w

let e, v, w be object ; :: thesis: ( e Joins v,w,G implies f . v <> f . w )
assume A2: e Joins v,w,G ; :: thesis: f . v <> f . w
then A3: v <> w by GLIB_000:18;
( v in the_Vertices_of G & w in the_Vertices_of G ) by A2, GLIB_000:13;
then ( v in dom f & w in dom f ) by PARTFUN1:def 2;
hence f . v <> f . w by A1, A3, FUNCT_1:def 4; :: thesis: verum

end;

hence f is proper by Th10; :: thesis: verum