let G, G1 be _Graph; :: thesis: for f being VColoring of G
for F being PGraphMapping of G1,G
for f9 being VColoring of G1 st F is total & f9 = f * (F _V) & f is proper holds
f9 is proper
let f be VColoring of G; :: thesis: for F being PGraphMapping of G1,G
for f9 being VColoring of G1 st F is total & f9 = f * (F _V) & f is proper holds
f9 is proper
let F be PGraphMapping of G1,G; :: thesis: for f9 being VColoring of G1 st F is total & f9 = f * (F _V) & f is proper holds
f9 is proper
let f9 be VColoring of G1; :: thesis: ( F is total & f9 = f * (F _V) & f is proper implies f9 is proper )
assume A1: ( F is total & f9 = f * (F _V) & f is proper ) ; :: thesis: f9 is proper

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

let e, v, w be object ; :: thesis: ( e Joins v,w,G1 implies f9 . v <> f9 . w )
assume A2: e Joins v,w,G1 ; :: thesis: f9 . v <> f9 . w
then ( e in the_Edges_of G1 & v in the_Vertices_of G1 & w in the_Vertices_of G1 ) by GLIB_000:def 13, GLIB_000:13;
then A3: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) by A1, GLIB_010:def 11;
then (F _E) . e Joins (F _V) . v,(F _V) . w,G by A2, GLIB_010:4;
then f . ((F _V) . v) <> f . ((F _V) . w) by A1, Th10;
then (f * (F _V)) . v <> f . ((F _V) . w) by A3, FUNCT_1:13;
hence f9 . v <> f9 . w by A1, A3, FUNCT_1:13; :: thesis: verum

end;

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