let f be homogeneous Function; :: thesis: ( f is binary implies not f is empty )
assume arity f = 2 ; :: according to COMPUT_1:def 26 :: 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