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