:: deftheorem Def8868 defines Sigma_tauhelp3 FINANCE5:def 22 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for tau being StoppingTime_Func of Sigma,MyFunc
for A1 being SetSequence of Omega
for t being Element of S
for b₈ being SetSequence of El_Filtration (t,MyFunc) holds
( b₈ = Sigma_tauhelp3 (MyFunc,tau,A1,t) iff for n being Nat holds b₈ . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t) );