set f = the VColoring of G;
set g = the EColoring of G;
take [ the VColoring of G, the EColoring of G] ; :: thesis: ex f being VColoring of G ex g being EColoring of G st [ the VColoring of G, the EColoring of G] = [f,g]
take the VColoring of G ; :: thesis: ex g being EColoring of G st [ the VColoring of G, the EColoring of G] = [ the VColoring of G,g]
take the EColoring of G ; :: thesis: [ the VColoring of G, the EColoring of G] = [ the VColoring of G, the EColoring of G]
thus [ the VColoring of G, the EColoring of G] = [ the VColoring of G, the EColoring of G] ; :: thesis: verum