let A be set ; :: thesis: {} is Function of A, {}

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

suppose A = {} ; :: thesis: {} is Function of A, {}

hence {} is Function of A, {} by RELSET_1:25; :: thesis: verum

end;

suppose A <> {} ; :: thesis: {} is Function of A, {}

hence {} is Function of A, {} by FUNCT_2:def 1, RELSET_1:25; :: thesis: verum

end;

end;