consider f being VColoring of G, g being EColoring of G such that
A2: t = [f,g] by Def9;
thus _E is EColoring of G by A2; :: thesis: verum