let y be object ; :: according to HILB10_7:def 6 :: thesis: card ((n |-> x) " {y}) is even

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

suppose y = x ; :: thesis: card ((n |-> x) " {y}) is even

then (n |-> x) " {y} = Seg n by FUNCOP_1:15;
hence card ((n |-> x) " {y}) is even ; :: thesis: verum

end;

suppose y <> x ; :: thesis: card ((n |-> x) " {y}) is even

then not x in {y} by TARSKI:def 1;
then (n |-> x) " {y} = {} by FUNCOP_1:16;
hence card ((n |-> x) " {y}) is even ; :: thesis: verum

end;

end;