let G1, G2 be _Graph; :: thesis: for g1 being EColoring of G1
for g2 being EColoring of G2 st G1 == G2 & g1 = g2 & g1 is proper holds
g2 is proper
let g1 be EColoring of G1; :: thesis: for g2 being EColoring of G2 st G1 == G2 & g1 = g2 & g1 is proper holds
g2 is proper
let g2 be EColoring of G2; :: thesis: ( G1 == G2 & g1 = g2 & g1 is proper implies g2 is proper )
assume A1: ( G1 == G2 & g1 = g2 & g1 is proper ) ; :: thesis: g2 is proper
let v be Vertex of G2; :: according to GLCOLO00:def 5 :: thesis: g2 | (v .edgesInOut()) is one-to-one
reconsider w = v as Vertex of G1 by A1, GLIB_000:def 34;
v .edgesInOut() = w .edgesInOut() by A1, GLIB_000:96;
hence g2 | (v .edgesInOut()) is one-to-one by A1; :: thesis: verum