let G1, G2 be _Graph; :: thesis: for c being Cardinal st G1 == G2 & G1 is c -vcolorable holds
G2 is c -vcolorable
let c be Cardinal; :: thesis: ( G1 == G2 & G1 is c -vcolorable implies G2 is c -vcolorable )
assume A1: ( G1 == G2 & G1 is c -vcolorable ) ; :: thesis: G2 is c -vcolorable
then consider f1 being VColoring of G1 such that
A2: ( f1 is proper & card (rng f1) c= c ) ;
the_Vertices_of G1 = the_Vertices_of G2 by A1, GLIB_000:def 34;
then reconsider f2 = f1 as VColoring of G2 ;
f2 is proper by A1, A2, Th16;
hence G2 is c -vcolorable by A2; :: thesis: verum