:: deftheorem Def7 defines TrivialOp PRALG_1:def 7 :
for k being Nat
for b₂ being PartFunc of ({{}} *),{{}} holds
( b₂ = TrivialOp k iff ( dom b₂ = {(k |-> {})} & rng b₂ = {{}} ) );