let G be _Graph; :: thesis: for f being VColoring of G
for H being Subgraph of G
for f9 being VColoring of H st f9 = f | (the_Vertices_of H) & f is proper holds
f9 is proper
let f be VColoring of G; :: thesis: for H being Subgraph of G
for f9 being VColoring of H st f9 = f | (the_Vertices_of H) & f is proper holds
f9 is proper
let H be Subgraph of G; :: thesis: for f9 being VColoring of H st f9 = f | (the_Vertices_of H) & f is proper holds
f9 is proper
let f9 be VColoring of H; :: thesis: ( f9 = f | (the_Vertices_of H) & f is proper implies f9 is proper )
assume A1: ( f9 = f | (the_Vertices_of H) & f is proper ) ; :: thesis: f9 is proper

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

let e, v, w be object ; :: thesis: ( e Joins v,w,H implies f9 . v <> f9 . w )
assume A2: e Joins v,w,H ; :: thesis: f9 . v <> f9 . w
( v is set & w is set ) by TARSKI:1;
then A3: f . v <> f . w by A1, A2, Th10, GLIB_000:72;
( v in the_Vertices_of H & w in the_Vertices_of H ) by A2, GLIB_000:13;
then ( v in dom f9 & w in dom f9 ) by PARTFUN1:def 2;
then ( f . v = f9 . v & f . w = f9 . w ) by A1, FUNCT_1:47;
hence f9 . v <> f9 . w by A3; :: thesis: verum

end;

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