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

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

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;