:: deftheorem Def8868 defines Sigma_tauhelp3 FINANCE5:def 10 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for tau being StoppingTime_Func of MyFunc
for A being SetSequence of Omega
for t being Element of I
for b₉ being SetSequence of El_Filtration (t,MyFunc) holds
( b₉ = Sigma_tauhelp3 (tau,A,t) iff for n being Nat holds b₉ . n = Sigma_tauhelp2 (tau,A,n,t) );