let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for s being real number holds Omega --> s is_random_variable_on Sigma, Borel_Sets
let Sigma be SigmaField of Omega; :: thesis: for s being real number holds Omega --> s is_random_variable_on Sigma, Borel_Sets
let s be real number ; :: thesis: Omega --> s is_random_variable_on Sigma, Borel_Sets
set X = Omega --> s;
Omega --> s is_random_variable_on Sigma, Borel_Sets

proof

let x be Element of Borel_Sets ; :: according to FINANCE1:def 5 :: thesis: { y where y is Element of Omega : (Omega --> s) . y is Element of x } is Element of Sigma

per cases ( s is Element of x or not s is Element of x ) ;

suppose SJ0: s is Element of x ; :: thesis: { y where y is Element of Omega : (Omega --> s) . y is Element of x } is Element of Sigma

for q being set holds
( q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } iff q in Omega )

proof

let q be set ; :: thesis: ( q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } iff q in Omega )

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

assume q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } ; :: thesis: q in Omega
then ex w being Element of Omega st
( w = q & (Omega --> s) . 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 : (Omega --> s) . w is Element of x }
then reconsider w = q as Element of Omega ;
(Omega --> s) . w is Element of x by SJ0, FUNCOP_1:7;
hence q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } ; :: thesis: verum

end;

then { w where w is Element of Omega : (Omega --> s) . w is Element of x } = Omega by TARSKI:1;
hence { y where y is Element of Omega : (Omega --> s) . y is Element of x } is Element of Sigma by PROB_1:23; :: thesis: verum

end;

suppose IIII: s is not Element of x ; :: thesis: { y where y is Element of Omega : (Omega --> s) . y is Element of x } is Element of Sigma

for q being set holds
( q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } iff q in {} )

proof

let q be set ; :: thesis: ( q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } iff q in {} )

now

assume q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } ; :: thesis: q in {}
then consider w being Element of Omega such that
TTJ0: ( w = q & (Omega --> s) . w is Element of x ) ;
thus q in {} by IIII, TTJ0, FUNCOP_1:7; :: thesis: verum

end;

hence ( q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } iff q in {} ) ; :: thesis: verum

end;

then { w where w is Element of Omega : (Omega --> s) . w is Element of x } = {} by TARSKI:1;
hence { y where y is Element of Omega : (Omega --> s) . y is Element of x } is Element of Sigma by PROB_1:22; :: thesis: verum

end;

end;

end;

hence Omega --> s is_random_variable_on Sigma, Borel_Sets ; :: thesis: verum