let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for t2 being Element of I ex q being random_variable of Sigma, BorelSubsets I st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc )

let Sigma be SigmaField of Omega; :: thesis: for r being Real
for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for t2 being Element of I ex q being random_variable of Sigma, BorelSubsets I st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc )

let r be Real; :: thesis: for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for t2 being Element of I ex q being random_variable of Sigma, BorelSubsets I st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc )

let I be TheEvent of r; :: thesis: for MyFunc being Filtration of I,Sigma
for t2 being Element of I ex q being random_variable of Sigma, BorelSubsets I st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc )

let MyFunc be Filtration of I,Sigma; :: thesis: for t2 being Element of I ex q being random_variable of Sigma, BorelSubsets I st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc )

let t2 be Element of I; :: thesis: ex q being random_variable of Sigma, BorelSubsets I st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc )

set Sigma2 = BorelSubsets I;
Fin1: for t being Element of I holds { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFunc . t
proof
let t be Element of I; :: thesis: { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFunc . t
set WW = { w where w is Element of Omega : (Omega --> t2) . w <= t } ;
reconsider MyFt = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;
per cases ( t2 <= t or t2 > t ) ;
suppose S1: t2 <= t ; :: thesis: { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFunc . t
H1: for x being object st x in { w where w is Element of Omega : (Omega --> t2) . w <= t } holds
x in Omega
proof
let x be object ; :: thesis: ( x in { w where w is Element of Omega : (Omega --> t2) . w <= t } implies x in Omega )
assume x in { w where w is Element of Omega : (Omega --> t2) . w <= t } ; :: thesis: x in Omega
then ex w3 being Element of Omega st
( w3 = x & (Omega --> t2) . w3 <= t ) ;
hence x in Omega ; :: thesis: verum
end;
{ w where w is Element of Omega : (Omega --> t2) . w <= t } = Omega
proof
for x being object st x in Omega holds
x in { w where w is Element of Omega : (Omega --> t2) . w <= t }
proof
let x be object ; :: thesis: ( x in Omega implies x in { w where w is Element of Omega : (Omega --> t2) . w <= t } )
assume x in Omega ; :: thesis: x in { w where w is Element of Omega : (Omega --> t2) . w <= t }
then reconsider x = x as Element of Omega ;
(Omega --> t2) . x = t2 by FUNCOP_1:7;
hence x in { w where w is Element of Omega : (Omega --> t2) . w <= t } by S1; :: thesis: verum
end;
hence { w where w is Element of Omega : (Omega --> t2) . w <= t } = Omega by ; :: thesis: verum
end;
then { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFt by PROB_1:5;
hence { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFunc . t ; :: thesis: verum
end;
suppose S1: t2 > t ; :: thesis: { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFunc . t
{ w where w is Element of Omega : (Omega --> t2) . w <= t } c= {}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of Omega : (Omega --> t2) . w <= t } or x in {} )
assume x in { w where w is Element of Omega : (Omega --> t2) . w <= t } ; :: thesis: x in {}
then ex w3 being Element of Omega st
( w3 = x & (Omega --> t2) . w3 <= t ) ;
hence x in {} by ; :: thesis: verum
end;
then { w where w is Element of Omega : (Omega --> t2) . w <= t } = {} ;
then { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFt by PROB_1:4;
hence { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFunc . t ; :: thesis: verum
end;
end;
end;
set OC = Omega --> t2;
Omega --> t2 is random_variable of Sigma, BorelSubsets I by FINANCE3:10;
then reconsider OC = Omega --> t2 as random_variable of Sigma, BorelSubsets I ;
OC is_StoppingTime_wrt MyFunc by Fin1;
hence ex q being random_variable of Sigma, BorelSubsets I st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc ) ; :: thesis: verum