theorem THJ1:
for
Omega being non
empty set for
Sigma being
SigmaField of
Omega for
Sigma2 being
SigmaField of
{1} st
Omega = {1,2,3,4} holds
ex
X1 being
Function of
Omega,
{1} st
(
X1 is
random_variable of
Special_SigmaField1 ,
Sigma2 &
X1 is
random_variable of
Special_SigmaField2 ,
Sigma2 &
X1 is
random_variable of
Trivial-SigmaField {1,2,3,4},
Sigma2 )