let Omega be non empty set ; :: thesis: for Sigma4 being SigmaField of Omega
for Sigma5 being SigmaField of {1} holds Omega --> 1 is random_variable of Sigma4,Sigma5
let Sigma4 be SigmaField of Omega; :: thesis: for Sigma5 being SigmaField of {1} holds Omega --> 1 is random_variable of Sigma4,Sigma5
let Sigma5 be SigmaField of {1}; :: thesis: Omega --> 1 is random_variable of Sigma4,Sigma5
set 1REAL = 1;
reconsider 1REAL = 1 as Real ;
reconsider X = Omega --> 1REAL as Function of Omega,{1} ;
X is Sigma4,Sigma5 -random_variable-like

proof

let x be set ; :: according to FINANCE1:def 5 :: thesis: ( not x in Sigma5 or X " x in Sigma4 )

per cases ( 1 in x or not 1 in x ) ;

suppose A1: 1 in x ; :: thesis: ( not x in Sigma5 or X " x in Sigma4 )

for q being object holds
( q in { w where w is Element of Omega : X . w is Element of x } iff q in Omega )

proof

let q be object ; :: thesis: ( q in { w where w is Element of Omega : X . w is Element of x } iff q in Omega )

hereby :: thesis: ( q in Omega implies q in { w where w is Element of Omega : X . w is Element of x } )

assume q in { w where w is Element of Omega : X . w is Element of x } ; :: thesis: q in Omega
then ex w being Element of Omega st
( w = q & X . w is Element of x ) ;
hence q in Omega ; :: thesis: verum

end;

assume q in Omega ; :: thesis: q in { w where w is Element of Omega : X . w is Element of x }
then reconsider w = q as Element of Omega ;
X . w is Element of x by A1, FUNCOP_1:7;
hence q in { w where w is Element of Omega : X . w is Element of x } ; :: thesis: verum

end;

then A2: { w where w is Element of Omega : X . w is Element of x } = Omega by TARSKI:2;
{ w where w is Element of Omega : X . w is Element of x } = X " x by A1, Lm1A;
then X " x is Element of Sigma4 by A2, PROB_1:23;
hence ( not x in Sigma5 or X " x in Sigma4 ) ; :: thesis: verum

end;

suppose A3: not 1 in x ; :: thesis: ( not x in Sigma5 or X " x in Sigma4 )

X " x c= {}

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in X " x or q in {} )
assume q in X " x ; :: thesis: q in {}
then ( q in dom X & X . q in x ) by FUNCT_1:def 7;
hence q in {} by A3, FUNCOP_1:7; :: thesis: verum

end;

then X " x = {} ;
then X " x is Element of Sigma4 by PROB_1:22;
hence ( not x in Sigma5 or X " x in Sigma4 ) ; :: thesis: verum

end;

end;

end;

hence Omega --> 1 is random_variable of Sigma4,Sigma5 ; :: thesis: verum