let V be set ; :: thesis: for G2 being _Graph
for G1 being addVertices of G2,V
for f1 being VColoring of G1
for f2 being VColoring of G2
for h being Function st dom h = V \ (the_Vertices_of G2) & f1 = f2 +* h & f2 is proper holds
f1 is proper
let G2 be _Graph; :: thesis: for G1 being addVertices of G2,V
for f1 being VColoring of G1
for f2 being VColoring of G2
for h being Function st dom h = V \ (the_Vertices_of G2) & f1 = f2 +* h & f2 is proper holds
f1 is proper
let G1 be addVertices of G2,V; :: thesis: for f1 being VColoring of G1
for f2 being VColoring of G2
for h being Function st dom h = V \ (the_Vertices_of G2) & f1 = f2 +* h & f2 is proper holds
f1 is proper
let f1 be VColoring of G1; :: thesis: for f2 being VColoring of G2
for h being Function st dom h = V \ (the_Vertices_of G2) & f1 = f2 +* h & f2 is proper holds
f1 is proper
let f2 be VColoring of G2; :: thesis: for h being Function st dom h = V \ (the_Vertices_of G2) & f1 = f2 +* h & f2 is proper holds
f1 is proper
let h be Function; :: thesis: ( dom h = V \ (the_Vertices_of G2) & f1 = f2 +* h & f2 is proper implies f1 is proper )
assume A1: ( dom h = V \ (the_Vertices_of G2) & f1 = f2 +* h & f2 is proper ) ; :: thesis: f1 is proper

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

let e, v, w be object ; :: thesis: ( e Joins v,w,G1 implies f1 . v <> f1 . w )
assume e Joins v,w,G1 ; :: thesis: f1 . v <> f1 . w
then A2: e Joins v,w,G2 by GLIB_006:87;
( v in the_Vertices_of G2 & w in the_Vertices_of G2 ) by A2, GLIB_000:13;
then ( not v in dom h & not w in dom h ) by A1, XBOOLE_0:def 5;
then ( f1 . v = f2 . v & f1 . w = f2 . w ) by A1, FUNCT_4:11;
hence f1 . v <> f1 . w by A1, A2, Th10; :: thesis: verum

end;

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