set f = the proper VColoring of G;
set g9 = the proper EColoring of G;
consider g being proper EColoring of G such that
A1: ( rng the proper VColoring of G misses rng g & card (rng the proper EColoring of G) = card (rng g) ) by Th149;
reconsider t = [ the proper VColoring of G,g] as TColoring of G ;
take t ; :: thesis: t is proper
thus t is proper by A1, Th147; :: thesis: verum