per cases ( A <> {} or A = {} ) ;
suppose A <> {} ; :: thesis: f . (a,b) is Element of A
then reconsider A = A as non empty set ;
reconsider f = f as BinOp of A ;
reconsider ab = [a,b] as Element of [:A,A:] by ZFMISC_1:def 2;
f . ab is Element of A ;
hence f . (a,b) is Element of A ; :: thesis: verum
end;
suppose A1: A = {} ; :: thesis: f . (a,b) is Element of A
then not [a,b] in dom f ;
then f . (a,b) = {} by FUNCT_1:def 2;
hence f . (a,b) is Element of A by A1, SUBSET_1:def 1; :: thesis: verum
end;
end;