theorem MyFunc5:
for
k1,
k2,
k3,
k4 being
Element of
REAL 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 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
eli being
Element of
I st
eli = 3 holds
ex
f being
Function of
Omega,
REAL st
(
f . 1
= k1 &
f . 2
= k2 &
f . 3
= k3 &
f . 4
= k4 &
f is
El_Filtration (
eli,
MyFunc),
Borel_Sets -random_variable-like )