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;