theorem
for
Omega being non
empty set st
Omega = {1,2,3,4} holds
for
Sigma being
SigmaField of
Omega for
I being non
empty real-membered set st
I = {1,2,3} &
Sigma = bool {1,2,3,4} holds
for
MyFunc being
ManySortedSigmaField of
I,
Sigma st
MyFunc . 1
= Special_SigmaField1 &
MyFunc . 2
= Special_SigmaField2 &
MyFunc . 3
= Trivial-SigmaField {1,2,3,4} holds
for
Prob being
Function of
Sigma,
REAL for
i being
Element of
I ex
RV being
Function of
Omega,
REAL st
RV is
El_Filtration (
i,
MyFunc),
Borel_Sets -random_variable-like