let G1, G2 be _Graph; :: thesis: for f1 being VColoring of G1
for f2 being VColoring of G2 st G1 == G2 & f1 = f2 & f1 is proper holds
f2 is proper
let f1 be VColoring of G1; :: thesis: for f2 being VColoring of G2 st G1 == G2 & f1 = f2 & f1 is proper holds
f2 is proper
let f2 be VColoring of G2; :: thesis: ( G1 == G2 & f1 = f2 & f1 is proper implies f2 is proper )
assume A1: ( G1 == G2 & f1 = f2 & f1 is proper ) ; :: thesis: f2 is proper

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

let e, v, w be object ; :: thesis: ( e Joins v,w,G2 implies f2 . v <> f2 . w )
assume e Joins v,w,G2 ; :: thesis: f2 . v <> f2 . w
then e Joins v,w,G1 by A1, GLIB_000:88;
hence f2 . v <> f2 . w by A1, Th10; :: thesis: verum

end;

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