let Omega, Omega2 be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for s being Element of Omega2 holds Omega --> s is Sigma,Sigma2 -random_variable-like
let Sigma be SigmaField of Omega; :: thesis: for Sigma2 being SigmaField of Omega2
for s being Element of Omega2 holds Omega --> s is Sigma,Sigma2 -random_variable-like
let Sigma2 be SigmaField of Omega2; :: thesis: for s being Element of Omega2 holds Omega --> s is Sigma,Sigma2 -random_variable-like
let s be Element of Omega2; :: thesis: Omega --> s is Sigma,Sigma2 -random_variable-like
set X = Omega --> s;
let x be set ; :: according to FINANCE1:def 5 :: thesis: ( not x in Sigma2 or (Omega --> s) " x in Sigma )
per cases ( s in x or not s in x ) ;
suppose A1: s in x ; :: thesis: ( not x in Sigma2 or (Omega --> s) " x in Sigma )
for q being object 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 object ; :: 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 A1, 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:2;
then (Omega --> s) " x = Omega by A1, Lm1B;
then (Omega --> s) " x is Element of Sigma by PROB_1:23;
hence ( not x in Sigma2 or (Omega --> s) " x in Sigma ) ; :: thesis: verum
end;
suppose A3: not s in x ; :: thesis: ( not x in Sigma2 or (Omega --> s) " x in Sigma )
(Omega --> s) " x c= {}
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in (Omega --> s) " x or q in {} )
assume q in (Omega --> s) " x ; :: thesis: q in {}
then ( q in dom (Omega --> s) & (Omega --> s) . q in x ) by FUNCT_1:def 7;
hence q in {} by A3, FUNCOP_1:7; :: thesis: verum
end;
then (Omega --> s) " x = {} ;
then (Omega --> s) " x is Element of Sigma by PROB_1:22;
hence ( not x in Sigma2 or (Omega --> s) " x in Sigma ) ; :: thesis: verum
end;
end;