let G be _Graph; :: thesis: for f being VColoring of G
for g being EColoring of G st f is proper holds
ex f9 being VColoring of G st
( f9 is proper & rng f9 misses rng g & card (rng f) = card (rng f9) )
let f be VColoring of G; :: thesis: for g being EColoring of G st f is proper holds
ex f9 being VColoring of G st
( f9 is proper & rng f9 misses rng g & card (rng f) = card (rng f9) )
let g be EColoring of G; :: thesis: ( f is proper implies ex f9 being VColoring of G st
( f9 is proper & rng f9 misses rng g & card (rng f) = card (rng f9) ) )
assume A1: f is proper ; :: thesis: ex f9 being VColoring of G st
( f9 is proper & rng f9 misses rng g & card (rng f) = card (rng f9) )
set h = <:((rng f) --> (rng g)),(id (rng f)):>;
set f9 = <:((rng f) --> (rng g)),(id (rng f)):> * f;
A2: dom <:((rng f) --> (rng g)),(id (rng f)):> = rng f by Lm8;
then reconsider f9 = <:((rng f) --> (rng g)),(id (rng f)):> * f as VColoring of G by Th1;
take f9 ; :: thesis: ( f9 is proper & rng f9 misses rng g & card (rng f) = card (rng f9) )
thus f9 is proper by A1, A2, Th12; :: thesis: ( rng f9 misses rng g & card (rng f) = card (rng f9) )
A3: rng f9 = rng <:((rng f) --> (rng g)),(id (rng f)):> by A2, RELAT_1:28;
hence rng f9 misses rng g by Lm11; :: thesis: card (rng f) = card (rng f9)
thus card (rng f) = card [:(rng f),{(rng g)}:] by CARD_1:69
.= card [:{(rng g)},(rng f):] by CARD_2:4
.= card (rng f9) by A3, Lm10 ; :: thesis: verum