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

A1: MySigmatau is compl-closed

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

{ 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

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

A1: MySigmatau is compl-closed

proof

A2:
MySigmatau is sigma-multiplicative
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

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

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

.= { 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;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

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

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

then Omega \ A in Sigma by PROB_1:6;

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

proof

K0:
for t being Element of S holds { 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

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

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

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

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

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

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

set CA = Complement A1;
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 }

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

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

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

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

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

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

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

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

proof

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

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