let f be homogeneous Function; :: thesis: ( f is unary implies not f is empty )
assume arity f = 1 ; :: according to COMPUT_1:def 25 :: thesis: not f is empty
then ex x being FinSequence st x in dom f by UNIALG_1:def 10;
hence not f is empty ; :: thesis: verum