let y be object ; :: according to FUNCT_1:def 9 :: thesis: ( not y in dom <%x%> or not <%x%> . y is empty )
assume y in dom <%x%> ; :: thesis: not <%x%> . y is empty
then y in 1 by AFINSQ_1:def 4;
then y = 0 by CARD_1:49, TARSKI:def 1;
hence not <%x%> . y is empty ; :: thesis: verum