let f be homogeneous Function; :: thesis: ( f is ternary implies not f is empty )
assume arity f = 3 ; :: according to COMPUT_1:def 27 :: thesis: not f is empty
then ex x being FinSequence st x in dom f by MARGREL1:def 26;
hence not f is empty ; :: thesis: verum