:: deftheorem Def12 defines Trivial-SigmaField_sequence RANDOM_3:def 12 :
for D being non-empty finite-yielding ManySortedSet of NAT
for b₂ being SigmaField_sequence of D holds
( b₂ = Trivial-SigmaField_sequence D iff for n being Nat holds b₂ . n = Trivial-SigmaField (D . n) );