let G1 be _Graph; :: thesis: for G2 being removeParallelEdges of G1 holds G1 .vChromaticNum() = G2 .vChromaticNum()
let G2 be removeParallelEdges of G1; :: thesis: G1 .vChromaticNum() = G2 .vChromaticNum()

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

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

then ( G1 .vChromaticNum() = 0 & G2 .vChromaticNum() = 0 ) ;
hence G1 .vChromaticNum() = G2 .vChromaticNum() ; :: thesis: verum

end;

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

then ( G2 is G1 .vChromaticNum() -vcolorable & ( for c being Cardinal st G2 is c -vcolorable holds
G1 .vChromaticNum() c= c ) ) by Th40, Th54, Th57;
hence G1 .vChromaticNum() = G2 .vChromaticNum() by Th58; :: thesis: verum

end;

end;