let f be homogeneous Function; :: thesis: ( f is n -ary implies not f is empty )
assume arity f = n ; :: according to COMPUT_1:def 21 :: thesis: not f is empty
then ex x being FinSequence st x in dom f by MARGREL1:def 25;
hence not f is empty ; :: thesis: verum