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