let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for T being Nat

for TFix being Element of StoppingSetExt T

for MyFunc being Filtration of StoppingSet T,Sigma holds Omega --> TFix is_StoppingTime_wrt MyFunc,T

let Sigma be SigmaField of Omega; :: thesis: for T being Nat

for TFix being Element of StoppingSetExt T

for MyFunc being Filtration of StoppingSet T,Sigma holds Omega --> TFix is_StoppingTime_wrt MyFunc,T

let T be Nat; :: thesis: for TFix being Element of StoppingSetExt T

for MyFunc being Filtration of StoppingSet T,Sigma holds Omega --> TFix is_StoppingTime_wrt MyFunc,T

let TFix be Element of StoppingSetExt T; :: thesis: for MyFunc being Filtration of StoppingSet T,Sigma holds Omega --> TFix is_StoppingTime_wrt MyFunc,T

let MyFunc be Filtration of StoppingSet T,Sigma; :: thesis: Omega --> TFix is_StoppingTime_wrt MyFunc,T

set const = Omega --> TFix;

for t being Element of StoppingSet T holds { w where w is Element of Omega : (Omega --> TFix) . w = t } in MyFunc . t

for T being Nat

for TFix being Element of StoppingSetExt T

for MyFunc being Filtration of StoppingSet T,Sigma holds Omega --> TFix is_StoppingTime_wrt MyFunc,T

let Sigma be SigmaField of Omega; :: thesis: for T being Nat

for TFix being Element of StoppingSetExt T

for MyFunc being Filtration of StoppingSet T,Sigma holds Omega --> TFix is_StoppingTime_wrt MyFunc,T

let T be Nat; :: thesis: for TFix being Element of StoppingSetExt T

for MyFunc being Filtration of StoppingSet T,Sigma holds Omega --> TFix is_StoppingTime_wrt MyFunc,T

let TFix be Element of StoppingSetExt T; :: thesis: for MyFunc being Filtration of StoppingSet T,Sigma holds Omega --> TFix is_StoppingTime_wrt MyFunc,T

let MyFunc be Filtration of StoppingSet T,Sigma; :: thesis: Omega --> TFix is_StoppingTime_wrt MyFunc,T

set const = Omega --> TFix;

for t being Element of StoppingSet T holds { w where w is Element of Omega : (Omega --> TFix) . w = t } in MyFunc . t

proof

hence
Omega --> TFix is_StoppingTime_wrt MyFunc,T
; :: thesis: verum
let t be Element of StoppingSet T; :: thesis: { w where w is Element of Omega : (Omega --> TFix) . w = t } in MyFunc . t

end;per cases
( t = TFix or t <> TFix )
;

end;

suppose S0:
t = TFix
; :: thesis: { w where w is Element of Omega : (Omega --> TFix) . w = t } in MyFunc . t

C1:
{ w where w is Element of Omega : (Omega --> TFix) . w = t } = Omega

hence { w where w is Element of Omega : (Omega --> TFix) . w = t } in MyFunc . t by C1, PROB_1:5; :: thesis: verum

end;proof

MyFunc . t is SigmaField of Omega
by KOLMOG01:def 2;
for x being object holds

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

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

proof

hence
{ w where w is Element of Omega : (Omega --> TFix) . w = t } = Omega
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in { w where w is Element of Omega : (Omega --> TFix) . w = t } iff x in Omega )

thus ( x in { w where w is Element of Omega : (Omega --> TFix) . w = t } implies x in Omega ) :: thesis: ( x in Omega implies x in { w where w is Element of Omega : (Omega --> TFix) . w = t } )

then consider y being Element of Omega such that

F10: ( y = x & y in Omega ) ;

( y in Omega implies t = (Omega --> TFix) . y ) by FUNCOP_1:7, S0;

hence x in { w where w is Element of Omega : (Omega --> TFix) . w = t } by F10; :: thesis: verum

end;thus ( x in { w where w is Element of Omega : (Omega --> TFix) . w = t } implies x in Omega ) :: thesis: ( x in Omega implies x in { w where w is Element of Omega : (Omega --> TFix) . w = t } )

proof

assume
x in Omega
; :: thesis: x in { w where w is Element of Omega : (Omega --> TFix) . w = t }
assume
x in { w where w is Element of Omega : (Omega --> TFix) . w = t }
; :: thesis: x in Omega

then consider s being Element of Omega such that

E1: ( s = x & (Omega --> TFix) . s = t ) ;

thus x in Omega by E1; :: thesis: verum

end;then consider s being Element of Omega such that

E1: ( s = x & (Omega --> TFix) . s = t ) ;

thus x in Omega by E1; :: thesis: verum

then consider y being Element of Omega such that

F10: ( y = x & y in Omega ) ;

( y in Omega implies t = (Omega --> TFix) . y ) by FUNCOP_1:7, S0;

hence x in { w where w is Element of Omega : (Omega --> TFix) . w = t } by F10; :: thesis: verum

hence { w where w is Element of Omega : (Omega --> TFix) . w = t } in MyFunc . t by C1, PROB_1:5; :: thesis: verum

suppose S1:
t <> TFix
; :: thesis: { w where w is Element of Omega : (Omega --> TFix) . w = t } in MyFunc . t

c1:
{ w where w is Element of Omega : (Omega --> TFix) . w = t } c= {}

then {} in MyFunc . t by PROB_1:4;

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

end;proof

MyFunc . t is SigmaField of Omega
by KOLMOG01:def 2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of Omega : (Omega --> TFix) . w = t } or x in {} )

assume x in { w where w is Element of Omega : (Omega --> TFix) . w = t } ; :: thesis: x in {}

then ex s being Element of Omega st

( s = x & (Omega --> TFix) . s = t ) ;

then consider s being Element of Omega such that

E1: ( s = x & (Omega --> TFix) . s <> TFix ) by S1;

thus x in {} by E1, FUNCOP_1:7; :: thesis: verum

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

then ex s being Element of Omega st

( s = x & (Omega --> TFix) . s = t ) ;

then consider s being Element of Omega such that

E1: ( s = x & (Omega --> TFix) . s <> TFix ) by S1;

thus x in {} by E1, FUNCOP_1:7; :: thesis: verum

then {} in MyFunc . t by PROB_1:4;

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