let G be _Graph; :: thesis: for g being EColoring of G
for g9 being one-to-one Function
for g2 being EColoring of G st g2 = g9 * g & g is proper holds
g2 is proper
let g be EColoring of G; :: thesis: for g9 being one-to-one Function
for g2 being EColoring of G st g2 = g9 * g & g is proper holds
g2 is proper
let g9 be one-to-one Function; :: thesis: for g2 being EColoring of G st g2 = g9 * g & g is proper holds
g2 is proper
let g2 be EColoring of G; :: thesis: ( g2 = g9 * g & g is proper implies g2 is proper )
assume A1: ( g2 = g9 * g & g is proper ) ; :: thesis: g2 is proper

now :: thesis: for v being Vertex of G holds g2 | (v .edgesInOut()) is one-to-one

let v be Vertex of G; :: thesis: g2 | (v .edgesInOut()) is one-to-one
set V = v .edgesInOut() ;
A2: g | (v .edgesInOut()) is one-to-one by A1;
g2 | (v .edgesInOut()) = g9 * (g | (v .edgesInOut())) by A1, RELAT_1:83;
hence g2 | (v .edgesInOut()) is one-to-one by A2; :: thesis: verum

end;

hence g2 is proper ; :: thesis: verum