per cases ( A = {} or A <> {} ) ;

suppose A1: A = {} ; :: thesis: f . x,y is Element of A

then [:A,A:] = {} by ZFMISC_1:113;
then dom f = {} ;
then f . x,y = {} by FUNCT_1:def 4;
hence f . x,y is Element of A by A1, SUBSET_1:def 2; :: thesis: verum

end;

suppose A <> {} ; :: thesis: f . x,y is Element of A

then reconsider A = A as non empty set ;
reconsider f = f as BinOp of A ;
reconsider x = x, y = y as Element of A ;
f . x,y is Element of A ;
hence f . x,y is Element of A ; :: thesis: verum

end;

end;