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

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

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

reconsider f = {} as PartFunc of A,{} by RELSET_1:12;
f is total by A1;
hence {} is Function of A,{} ; :: thesis: verum

end;

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

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

end;

end;