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

A1: MySigmatau is compl-closed

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

{ 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

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

A1: MySigmatau is compl-closed

proof

A2:
MySigmatau is sigma-multiplicative
for A being Subset of Omega st A in MySigmatau holds

A ` in MySigmatau

end;A ` in MySigmatau

proof

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

then Omega \ A in Sigma by PROB_1:6;

hence A ` in MySigmatau by GW2; :: thesis: verum

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

( Omega in Sigma & A in Sigma )
by PROB_1:5;
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 }

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

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

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

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

hence j in A ` by XBOOLE_0:def 5, Help2; :: thesis: verum

proof

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

end;j in { w where w is Element of Omega : tau . w <= t } \ (A /\ { w where w is Element of Omega : tau . w <= t } )

proof

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

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

then Omega \ A in Sigma by PROB_1:6;

hence A ` in MySigmatau by GW2; :: thesis: verum

proof

K1:
for t being Element of I holds Omega /\ { w2 where w2 is Element of Omega : tau . w2 <= t } in MyFunc . t
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

set CA = Complement A1;

for n being Nat holds (Complement A1) . n is Event of Sigma

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;assume ASSJ: rng A1 c= MySigmatau ; :: thesis: Intersection A1 in MySigmatau

TT1: for n being Nat holds A1 . n in MySigmatau

proof

QQ1:
for t being Element of I holds (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t
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;A1 . n in rng A1 by FUNCT_2:4, ORDINAL1:def 12;

hence A1 . n in MySigmatau by ASSJ; :: thesis: verum

proof

for n being Nat holds A1 . n is Event of Sigma
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 }

x in Union (Sigma_tauhelp3 (tau,A1,t))

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

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

H:
for x being object st x in (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t } holds
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;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

x in Union (Sigma_tauhelp3 (tau,A1,t))

proof

Union (Sigma_tauhelp3 (tau,A1,t)) = (Union (Complement A1)) /\ { w where w is Element of Omega : tau . w <= t }
by H, X1, TARSKI:2;
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;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

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

proof

then reconsider A1 = A1 as SetSequence of Sigma by PROB_1:25;
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;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

set CA = Complement A1;

for n being Nat holds (Complement A1) . n is Event of Sigma

proof

then reconsider CA = Complement A1 as SetSequence of Sigma by PROB_1:25;
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;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

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

proof

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

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