:: deftheorem Def8 defines TrivialOps PRALG_1:def 8 :
for f being FinSequence of NAT
for b₂ being PFuncFinSequence of {{}} holds
( b₂ = TrivialOps f iff ( len b₂ = len f & ( for n being Nat st n in dom b₂ holds
for m being Nat st m = f . n holds
b₂ . n = TrivialOp m ) ) );