let Z be Subset of REAL; :: thesis: ( not 0 in Z implies (id Z) " {0} = {} )
assume AA: not 0 in Z ; :: thesis: (id Z) " {0} = {}
(id Z) " {0} c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (id Z) " {0} or x in {} )
assume x in (id Z) " {0} ; :: thesis: x in {}
then A2: ( x in dom (id Z) & (id Z) . x in {0} ) by FUNCT_1:def 7;
then (id Z) . x = x by FUNCT_1:17;
hence x in {} by A2, AA, TARSKI:def 1; :: thesis: verum

end;

hence (id Z) " {0} = {} ; :: thesis: verum