:: deftheorem Def8 defines -SigmaField_sequence-like RANDOM_3:def 8 :
for S, F being ManySortedSet of NAT holds
( F is S -SigmaField_sequence-like iff for n being Nat holds F . n is SigmaField of (S . n) );