set xx = <*x,x*>;
let y be object ; :: according to HILB10_7:def 6 :: thesis: card (<*x,x*> " {y}) is even
rng <*x*> = {x} by FINSEQ_1:38;
then A1: rng <*x,x*> = {x} \/ {x} by FINSEQ_1:31;

per cases ( y = x or y <> x ) ;

suppose y = x ; :: thesis: card (<*x,x*> " {y}) is even

then <*x,x*> " {y} = dom <*x,x*> by A1, RELAT_1:134;
then card (<*x,x*> " {y}) = 2 * 1 by CARD_1:def 7;
hence card (<*x,x*> " {y}) is even ; :: thesis: verum

end;

suppose y <> x ; :: thesis: card (<*x,x*> " {y}) is even

then <*x,x*> " {y} = {} by A1, RELAT_1:138, ZFMISC_1:11;
hence card (<*x,x*> " {y}) is even ; :: thesis: verum

end;

end;