let G be _Graph; :: thesis: for f being VColoring of G
for f9 being one-to-one Function
for f2 being VColoring of G st f2 = f9 * f & f is proper & rng f c= dom f9 holds
f2 is proper
let f be VColoring of G; :: thesis: for f9 being one-to-one Function
for f2 being VColoring of G st f2 = f9 * f & f is proper & rng f c= dom f9 holds
f2 is proper
let f9 be one-to-one Function; :: thesis: for f2 being VColoring of G st f2 = f9 * f & f is proper & rng f c= dom f9 holds
f2 is proper
let f2 be VColoring of G; :: thesis: ( f2 = f9 * f & f is proper & rng f c= dom f9 implies f2 is proper )
assume A1: ( f2 = f9 * f & f is proper & rng f c= dom f9 ) ; :: thesis: f2 is proper

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

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

end;

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