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

Omega --> t2 is random_variable of Sigma, ExtBorelsubsets by FINANCE3:10;

then reconsider OC = Omega --> t2 as random_variable of Sigma, ExtBorelsubsets ;

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

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

set OC = Omega --> t2;
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

end;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;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

per cases
( t2 <= t or t2 > t )
;

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 } = Omega

hence { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFunc . t ; :: thesis: verum

end;proof

then
{ w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFt
by PROB_1:5;
for x being object st x in Omega holds

x in { w where w is Element of Omega : (Omega --> t2) . w <= t }

end;x in { w where w is Element of Omega : (Omega --> t2) . w <= t }

proof

hence
{ w where w is Element of Omega : (Omega --> t2) . w <= t } = Omega
by H1, TARSKI:2; :: thesis: verum
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;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

hence { w where w is Element of Omega : (Omega --> t2) . w <= t } in MyFunc . t ; :: thesis: verum

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= {}

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;proof

then
{ w where w is Element of Omega : (Omega --> t2) . w <= t } = {}
;
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;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

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

Omega --> t2 is random_variable of Sigma, ExtBorelsubsets by FINANCE3:10;

then reconsider OC = Omega --> t2 as random_variable of Sigma, ExtBorelsubsets ;

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