for f being FinSequence of NAT holds
( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty )