theorem Th9: :: PRALG_1:9

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