assume ((#Z 0) + (#Z 2)) " {0} <> {} ; :: thesis: contradiction
then consider x being object such that
A1: x in ((#Z 0) + (#Z 2)) " {0} by XBOOLE_0:def 1;
reconsider x = x as Element of REAL by A1;
((#Z 0) + (#Z 2)) . x in {0} by A1, FUNCT_1:def 7;
then 0 = ((#Z 0) + (#Z 2)) . x by TARSKI:def 1
.= 1 + (x * x) by Lm5 ;
hence contradiction ; :: thesis: verum