set MySigmatau = { A where A is Element of Sigma : for t being Element of I 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 I 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 I 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 I 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 I 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 I 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

for A being Subset of Omega st A in MySigmatau holds
A ` in MySigmatau

proof

let A be Subset of Omega; :: thesis: ( A in MySigmatau implies 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 I 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 I holds (A `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t

proof

let t be Element of I; :: thesis: (A `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t
reconsider MyFt2 = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;
WW0: for j being object st j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) holds
j in (A `) /\ { w where w is Element of Omega : tau . w <= t }

proof

let j be object ; :: thesis: ( j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) implies j in (A `) /\ { w where w is Element of Omega : tau . w <= t } )
assume h: j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) ; :: thesis: j in (A `) /\ { w where w is Element of Omega : tau . w <= t }
then Help00: ( j in { w where w is Element of Omega : tau . w <= t } & not j in A /\ { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 5;
then Help2: not j in A by XBOOLE_0:def 4;
j in A `

proof

ex w2 being Element of Omega st
( j = w2 & tau . w2 <= t ) by Help00;
hence j in A ` by XBOOLE_0:def 5, Help2; :: thesis: verum

end;

hence j in (A `) /\ { w where w is Element of Omega : tau . w <= t } by XBOOLE_0:def 4, h; :: 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 } ) = (A `) /\ { w where w is Element of Omega : tau . w <= t }

proof

for j being object st j in (A `) /\ { w where w is Element of Omega : tau . w <= t } holds
j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } )

proof

let j be object ; :: thesis: ( j in (A `) /\ { w where w is Element of Omega : tau . w <= t } implies j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) )
assume j in (A `) /\ { w where w is Element of Omega : tau . w <= t } ; :: thesis: j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } )
then hh: ( j in Omega \ A & j in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 4;
then ( j in Omega & not j in A & j in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 5;
then not j in A /\ { w where w is Element of Omega : tau . w <= t } by XBOOLE_0:def 4;
hence j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) by hh, XBOOLE_0:def 5; :: thesis: verum

end;

hence { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } ) = (A `) /\ { w where w is Element of Omega : tau . w <= t } by WW0, TARSKI:2; :: thesis: verum

end;

W2: A /\ { w where w is Element of Omega : tau . w <= t } is Event of MyFt2 by GW1;
tau is_StoppingTime_wrt MyFunc by Def1111;
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;

hence MySigmatau is compl-closed ; :: 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;

QQ1: for t being Element of I holds (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t

proof

let t be Element of I; :: thesis: (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t
X1: for x being object st x in Union (Sigma_tauhelp3 (tau,A1,t)) holds
x in (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t }

proof

let x be object ; :: thesis: ( x in Union (Sigma_tauhelp3 (tau,A1,t)) implies x in (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } )
assume x in Union (Sigma_tauhelp3 (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 (tau,A1,t)) . n by PROB_1:12;
x in Sigma_tauhelp2 (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;
x in Union (Complement A1) by PROB_1:12, ZWJ1;
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;

H: for x being object st x in (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } holds
x in Union (Sigma_tauhelp3 (tau,A1,t))

proof

let x be object ; :: thesis: ( x in (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } implies x in Union (Sigma_tauhelp3 (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 (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 ZWJ2: x in Sigma_tauhelp2 (tau,A1,n,t) by ASSJ, Def8869;
x in (Sigma_tauhelp3 (tau,A1,t)) . n by ZWJ2, Def8868;
hence x in Union (Sigma_tauhelp3 (tau,A1,t)) by PROB_1:12; :: thesis: verum

end;

Union (Sigma_tauhelp3 (tau,A1,t)) = (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } by H, X1, TARSKI:2;
hence (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t by PROB_1:17; :: 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 I 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 consider AJ being Element of Sigma such that
AB1: ( AJ = A1 . n & ( for t being Element of I 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;

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

proof

let t be Element of I; :: thesis: Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t
tau is MyFunc -StoppingTime-like ;
then tau is_StoppingTime_wrt MyFunc ;
then N1: { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t ;
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 I 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 I holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } is SigmaField of Omega by A1, A2; :: thesis: verum