:: deftheorem defines El_Filtration FINANCE3:def 10 :
for I, Omega being non empty set
for Sigma being SigmaField of Omega
for Filt being ManySortedSigmaField of I,Sigma
for i being Element of I holds El_Filtration (i,Filt) = Filt . i;