let G1, G2 be _Graph; :: thesis: for c being Cardinal st G1 == G2 & G1 is c -tcolorable holds
G2 is c -tcolorable
let c be Cardinal; :: thesis: ( G1 == G2 & G1 is c -tcolorable implies G2 is c -tcolorable )
assume A1: ( G1 == G2 & G1 is c -tcolorable ) ; :: thesis: G2 is c -tcolorable
then consider t1 being TColoring of G1 such that
A2: ( t1 is proper & card ((rng (t1 _V)) \/ (rng (t1 _E))) c= c ) ;
A3: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by A1, GLIB_000:def 34;
then reconsider f = t1 _V as VColoring of G2 ;
reconsider g = t1 _E as EColoring of G2 by A3;
reconsider t2 = [f,g] as TColoring of G2 ;
t2 is proper by A1, A2, Th152;
hence G2 is c -tcolorable by A2; :: thesis: verum