let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
G1 .tChromaticNum() = G2 .tChromaticNum()
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies G1 .tChromaticNum() = G2 .tChromaticNum() )
assume A1: F is isomorphism ; :: thesis: G1 .tChromaticNum() = G2 .tChromaticNum()

per cases ( not G1 is loopless or G1 is loopless ) ;

suppose not G1 is loopless ; :: thesis: G1 .tChromaticNum() = G2 .tChromaticNum()

then ( not G1 is loopless & not G2 is loopless ) by A1, GLIB_010:35;
then ( G1 .tChromaticNum() = 0 & G2 .tChromaticNum() = 0 ) ;
hence G1 .tChromaticNum() = G2 .tChromaticNum() ; :: thesis: verum

end;

suppose A2: G1 is loopless ; :: thesis: G1 .tChromaticNum() = G2 .tChromaticNum()

now :: thesis: ( G2 is G1 .tChromaticNum() -tcolorable & ( for c being Cardinal st G2 is c -tcolorable holds
G1 .tChromaticNum() c= c ) )

G1 is G1 .tChromaticNum() -tcolorable by A2, Th186;
hence G2 is G1 .tChromaticNum() -tcolorable by A1, Th177; :: thesis: for c being Cardinal st G2 is c -tcolorable holds
G1 .tChromaticNum() c= c
let c be Cardinal; :: thesis: ( G2 is c -tcolorable implies G1 .tChromaticNum() c= c )
assume G2 is c -tcolorable ; :: thesis: G1 .tChromaticNum() c= c
then G1 is c -tcolorable by A1, Th177;
hence G1 .tChromaticNum() c= c by Th189; :: thesis: verum

end;

hence G1 .tChromaticNum() = G2 .tChromaticNum() by Th190; :: thesis: verum

end;

end;