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

proof

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

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

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

proof

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

proof

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 } )

proof

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;

assume x in Omega ; :: thesis: 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;

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

end;

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

end;

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

proof

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;

MyFunc . t is SigmaField of Omega by KOLMOG01:def 2;
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;

end;

end;

hence Omega --> TFix is_StoppingTime_wrt MyFunc,T ; :: thesis: verum