let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for s being Real
for f being Function of Omega,REAL st f = Omega --> s holds
f is Sigma, Borel_Sets -random_variable-like

let Sigma be SigmaField of Omega; :: thesis: for s being Real
for f being Function of Omega,REAL st f = Omega --> s holds
f is Sigma, Borel_Sets -random_variable-like

let s be Real; :: thesis: for f being Function of Omega,REAL st f = Omega --> s holds
f is Sigma, Borel_Sets -random_variable-like

let X be Function of Omega,REAL; :: thesis: ( X = Omega --> s implies X is Sigma, Borel_Sets -random_variable-like )
assume A0: X = Omega --> s ; :: thesis: X is Sigma, Borel_Sets -random_variable-like
X is Sigma, Borel_Sets -random_variable-like
proof
let x be set ; :: according to FINANCE1:def 5 :: thesis: ( x in Borel_Sets implies X " x in Sigma )
per cases ( s in x or not s in x ) ;
suppose A1: s in x ; :: thesis: ( x in Borel_Sets implies X " x in Sigma )
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 ;
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;
not x is empty by A1;
then { w where w is Element of Omega : X . w is Element of x } = X " x by Lm1;
then X " x = Omega by A2;
then X " x is Element of Sigma by PROB_1:23;
hence ( x in Borel_Sets implies X " x in Sigma ) ; :: thesis: verum
end;
suppose A3: not s in x ; :: thesis: ( x in Borel_Sets implies X " x in Sigma )
for q being object holds
( q in X " x iff q in {} )
proof
let q be object ; :: thesis: ( q in X " x iff q in {} )
now :: thesis: ( q in X " x implies 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 ; :: thesis: verum
end;
hence ( q in X " x iff q in {} ) ; :: thesis: verum
end;
then X " x = {} by TARSKI:2;
then X " x is Element of Sigma by PROB_1:22;
hence ( x in Borel_Sets implies X " x in Sigma ) ; :: thesis: verum
end;
end;
end;
hence X is Sigma, Borel_Sets -random_variable-like ; :: thesis: verum