set MySigmatau = { A where A is Element of Sigma : for t being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } ;
{ A where A is Element of Sigma : for t being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } c= bool Omega

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Element of Sigma : for t being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } or x in bool Omega )
assume x in { A where A is Element of Sigma : for t being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } ; :: thesis: x in bool Omega
then ex A being Element of Sigma st
( x = A & ( for t being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t ) ) ;
hence x in bool Omega ; :: thesis: verum

end;

then reconsider MySigmatau = { A where A is Element of Sigma : for t being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } as Subset-Family of Omega ;
A1: MySigmatau is compl-closed

proof

let A be Subset of Omega; :: according to PROB_1:def 1 :: thesis: ( not A in MySigmatau or A ` in MySigmatau )
assume A in MySigmatau ; :: thesis: A ` in MySigmatau
then consider B being Element of Sigma such that
GW1: ( A = B & ( for t being Element of S holds B /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t ) ) ;
reconsider A = A as Element of Sigma by GW1;
GW2: for t being Element of S holds (A `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t

proof

let t be Element of S; :: thesis: (A `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t
set F = { w where w is Element of Omega : tau . w <= t } ;
reconsider MyFt2 = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;
LL: { w where w is Element of Omega : tau . w <= t } c= Omega

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { w where w is Element of Omega : tau . w <= t } or b in Omega )
assume b in { w where w is Element of Omega : tau . w <= t } ; :: thesis: b in Omega
then ex ww being Element of Omega st
( ww = b & tau . ww <= t ) ;
hence b in Omega ; :: thesis: verum

end;

E1: { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) = { w where w is Element of Omega : tau . w <= t } \ A by XBOOLE_1:47
.= { w where w is Element of Omega : tau . w <= t } /\ (A `) by SUBSET_1:13, LL ;
W2: A /\ { w where w is Element of Omega : tau . w <= t } is Event of MyFt2 by GW1;
tau is_StoppingTime_wrt MyFunc,S by Def11111;
then { w where w is Element of Omega : tau . w <= t } is Event of MyFt2 ;
then { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) is Event of MyFt2 by W2, PROB_1:24;
hence (A `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t by E1; :: thesis: verum

end;

( Omega in Sigma & A in Sigma ) by PROB_1:5;
then Omega \ A in Sigma by PROB_1:6;
hence A ` in MySigmatau by GW2; :: thesis: verum

end;

A2: MySigmatau is sigma-multiplicative

proof

let A1 be SetSequence of Omega; :: according to PROB_1:def 6 :: thesis: ( not rng A1 c= MySigmatau or Intersection A1 in MySigmatau )
assume ASSJ: rng A1 c= MySigmatau ; :: thesis: Intersection A1 in MySigmatau
TT1: for n being Nat holds A1 . n in MySigmatau

proof

let n be Nat; :: thesis: A1 . n in MySigmatau
A1 . n in rng A1 by FUNCT_2:4, ORDINAL1:def 12;
hence A1 . n in MySigmatau by ASSJ; :: thesis: verum

end;

for n being Nat holds A1 . n is Event of Sigma

proof

let n be Nat; :: thesis: A1 . n is Event of Sigma
A1 . n in MySigmatau by TT1;
then ex AJ being Element of Sigma st
( AJ = A1 . n & ( for t being Element of S holds AJ /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ) ) ;
hence A1 . n is Event of Sigma ; :: thesis: verum

end;

then reconsider A1 = A1 as SetSequence of Sigma by PROB_1:25;
set CA = Complement A1;
for n being Nat holds (Complement A1) . n is Event of Sigma

proof

let n be Nat; :: thesis: (Complement A1) . n is Event of Sigma
A1 . n in MySigmatau by TT1;
then ex AJ being Element of Sigma st
( AJ = A1 . n & ( for t being Element of S holds AJ /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ) ) ;
then ( A1 . n is Event of Sigma & Sigma is compl-closed ) ;
then (A1 . n) ` is Event of Sigma ;
hence (Complement A1) . n is Event of Sigma by PROB_1:def 2; :: thesis: verum

end;

then reconsider CA = Complement A1 as SetSequence of Sigma by PROB_1:25;
QQ1: for t being Element of S holds (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t

proof

let t be Element of S; :: thesis: (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t
set R = { w where w is Element of Omega : tau . w <= t } ;
Union (Sigma_tauhelp3 (MyFunc,tau,A1,t)) = (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t }

proof

thus Union (Sigma_tauhelp3 (MyFunc,tau,A1,t)) c= (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } :: according to XBOOLE_0:def 10 :: thesis: (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } c= Union (Sigma_tauhelp3 (MyFunc,tau,A1,t))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (Sigma_tauhelp3 (MyFunc,tau,A1,t)) or x in (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } )
assume x in Union (Sigma_tauhelp3 (MyFunc,tau,A1,t)) ; :: thesis: x in (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t }
then consider n being Nat such that
V1: x in (Sigma_tauhelp3 (MyFunc,tau,A1,t)) . n by PROB_1:12;
x in Sigma_tauhelp2 (MyFunc,tau,A1,n,t) by V1, Def8868;
then x in ((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } by ASSJ, Def8869;
then ZWJ1: ( x in (Complement A1) . n & x in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 4;
then x in Union (Complement A1) by PROB_1:12;
hence x in (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } by XBOOLE_0:def 4, ZWJ1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } or x in Union (Sigma_tauhelp3 (MyFunc,tau,A1,t)) )
assume x in (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } ; :: thesis: x in Union (Sigma_tauhelp3 (MyFunc,tau,A1,t))
then ZWJ1: ( x in Union (Complement A1) & x in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 4;
then consider n being Nat such that
ZWJ2: x in (Complement A1) . n by PROB_1:12;
x in ((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } by XBOOLE_0:def 4, ZWJ1, ZWJ2;
then x in Sigma_tauhelp2 (MyFunc,tau,A1,n,t) by ASSJ, Def8869;
then x in (Sigma_tauhelp3 (MyFunc,tau,A1,t)) . n by Def8868;
hence x in Union (Sigma_tauhelp3 (MyFunc,tau,A1,t)) by PROB_1:12; :: thesis: verum

end;

hence (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t by PROB_1:17; :: thesis: verum

end;

set CA = Complement A1;
for n being Nat holds (Complement A1) . n is Event of Sigma

proof

let n be Nat; :: thesis: (Complement A1) . n is Event of Sigma
A1 . n in MySigmatau by TT1;
then consider AJ being Element of Sigma such that
AB1: ( AJ = A1 . n & ( for t being Element of S holds AJ /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ) ) ;
( A1 . n is Event of Sigma & Sigma is compl-closed ) by AB1;
then (A1 . n) ` is Event of Sigma ;
hence (Complement A1) . n is Event of Sigma by PROB_1:def 2; :: thesis: verum

end;

then reconsider CA = Complement A1 as SetSequence of Sigma by PROB_1:25;
reconsider UCA = Union CA as Event of Sigma by PROB_1:26;
UCA in MySigmatau by QQ1;
hence Intersection A1 in MySigmatau by A1; :: thesis: verum

end;

K0: for t being Element of S holds { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t

proof

let t be Element of S; :: thesis: { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t
tau is MyFunc -StoppingTime-like ;
then tau is_StoppingTime_wrt MyFunc,S ;
hence { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ; :: thesis: verum

end;

K1: for t being Element of S holds Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t

proof

let t be Element of S; :: thesis: Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t
N1: { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t by K0;
reconsider MyFt = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;
Omega is Event of MyFt by PROB_1:5;
then Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } is Event of MyFt by PROB_1:19, N1;
hence Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ; :: thesis: verum

end;

( Omega is Element of Sigma & ( for t being Element of S holds Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ) ) by PROB_1:5, K1;
then Omega in MySigmatau ;
hence { A where A is Element of Sigma : for t being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } is SigmaField of Omega by A1, A2; :: thesis: verum