let G be _Graph; :: thesis: for c1, c2 being Cardinal st G is c1 -vcolorable & G is c2 -ecolorable holds
G is c1 +` c2 -tcolorable
let c1, c2 be Cardinal; :: thesis: ( G is c1 -vcolorable & G is c2 -ecolorable implies G is c1 +` c2 -tcolorable )
assume A1: ( G is c1 -vcolorable & G is c2 -ecolorable ) ; :: thesis: G is c1 +` c2 -tcolorable
then consider f9 being VColoring of G such that
A2: ( f9 is proper & card (rng f9) c= c1 ) ;
consider g being proper EColoring of G such that
A3: card (rng g) c= c2 by A1;
consider f being VColoring of G such that
A4: ( f is proper & rng f misses rng g & card (rng f9) = card (rng f) ) by A2, Th150;
reconsider t = [f,g] as TColoring of G ;
A5: t is proper by A4, Th147;
card ((rng (t _V)) \/ (rng (t _E))) = (card (rng (t _V))) +` (card (rng (t _E))) by A4, CARD_2:35;
then card ((rng (t _V)) \/ (rng (t _E))) c= c1 +` c2 by A2, A3, A4, CARD_2:83;
hence G is c1 +` c2 -tcolorable by A5; :: thesis: verum