let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for t2 being Element of [.0,+infty.] ex q being random_variable of Sigma, ExtBorelsubsets st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc,S )
let Sigma be SigmaField of Omega; :: thesis: for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for t2 being Element of [.0,+infty.] ex q being random_variable of Sigma, ExtBorelsubsets st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc,S )
let S be non empty Subset of REAL; :: thesis: for MyFunc being Filtration of S,Sigma
for t2 being Element of [.0,+infty.] ex q being random_variable of Sigma, ExtBorelsubsets st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc,S )
let MyFunc be Filtration of S,Sigma; :: thesis: for t2 being Element of [.0,+infty.] ex q being random_variable of Sigma, ExtBorelsubsets st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc,S )
let t2 be Element of [.0,+infty.]; :: thesis: ex q being random_variable of Sigma, ExtBorelsubsets st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc,S )
Fin1: for t being Element of S holds { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFunc . t

proof

let t be Element of S; :: thesis: { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFunc . t
reconsider MyFt = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;
set R = { w where w is Element of Omega : (Omega --> t2) . w <= 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;

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

{ 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 H1, TARSKI:2; :: 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 S1, FUNCOP_1:7; :: 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;
for x being set holds (Omega --> t2) " x in Sigma

proof

let x be set ; :: thesis: (Omega --> t2) " x in Sigma
( (Omega --> t2) " x = {} or (Omega --> t2) " x = Omega )

proof

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

suppose S1: t2 in x ; :: thesis: ( (Omega --> t2) " x = {} or (Omega --> t2) " x = Omega )

set W = { z where z is Element of Omega : (Omega --> t2) . z in x } ;
{ z where z is Element of Omega : (Omega --> t2) . z in x } = Omega

proof

thus { z where z is Element of Omega : (Omega --> t2) . z in x } c= Omega :: according to XBOOLE_0:def 10 :: thesis: Omega c= { z where z is Element of Omega : (Omega --> t2) . z in x }

proof

let x2 be object ; :: according to TARSKI:def 3 :: thesis: ( not x2 in { z where z is Element of Omega : (Omega --> t2) . z in x } or x2 in Omega )
assume x2 in { z where z is Element of Omega : (Omega --> t2) . z in x } ; :: thesis: x2 in Omega
then ex z being Element of Omega st
( x2 = z & (Omega --> t2) . z in x ) ;
hence x2 in Omega ; :: thesis: verum

end;

let x2 be object ; :: according to TARSKI:def 3 :: thesis: ( not x2 in Omega or x2 in { z where z is Element of Omega : (Omega --> t2) . z in x } )
assume KK: x2 in Omega ; :: thesis: x2 in { z where z is Element of Omega : (Omega --> t2) . z in x }
then (Omega --> t2) . x2 in x by S1, FUNCOP_1:7;
hence x2 in { z where z is Element of Omega : (Omega --> t2) . z in x } by KK; :: thesis: verum

end;

hence ( (Omega --> t2) " x = {} or (Omega --> t2) " x = Omega ) by S1, LOC1; :: thesis: verum

end;

suppose S1: not t2 in x ; :: thesis: ( (Omega --> t2) " x = {} or (Omega --> t2) " x = Omega )

for q being object holds
( q in (Omega --> t2) " x iff q in {} )

proof

let q be object ; :: thesis: ( q in (Omega --> t2) " x iff q in {} )

hereby :: thesis: ( q in {} implies q in (Omega --> t2) " x )

assume q in (Omega --> t2) " x ; :: thesis: q in {}
then ( q in dom (Omega --> t2) & (Omega --> t2) . q in x ) by FUNCT_1:def 7;
hence q in {} by S1, FUNCOP_1:7; :: thesis: verum

end;

thus ( q in {} implies q in (Omega --> t2) " x ) ; :: thesis: verum

end;

hence ( (Omega --> t2) " x = {} or (Omega --> t2) " x = Omega ) by TARSKI:2; :: thesis: verum

end;

end;

end;

hence (Omega --> t2) " x in Sigma by PROB_1:4, PROB_1:5; :: thesis: verum

end;

then Omega --> t2 is_random_variable_on Sigma, ExtBorelsubsets ;
then reconsider OC = Omega --> t2 as random_variable of Sigma, ExtBorelsubsets by RANDOM_3:def 1;
OC is_StoppingTime_wrt MyFunc,S by Fin1;
hence ex q being random_variable of Sigma, ExtBorelsubsets st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc,S ) ; :: thesis: verum