reconsider n = n as Element of NAT by ORDINAL1:def 12;

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

A1 . n in rng A1 by FUNCT_2:4;

then A1 . n in { A where A is Element of Sigma : for t2 being Element of I holds A /\ { w where w is Element of Omega : tau . w <= t2 } in MyFunc . t2 } by LOC1;

then consider B being Element of Sigma such that

GW1: ( A1 . n = B & ( for t2 being Element of I holds B /\ { w where w is Element of Omega : tau . w <= t2 } in MyFunc . t2 ) ) ;

reconsider A1n = A1 . n as Element of Sigma by GW1;

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

hence ((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } is Element of El_Filtration (t,MyFunc) by GW2; :: thesis: verum

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

A1 . n in rng A1 by FUNCT_2:4;

then A1 . n in { A where A is Element of Sigma : for t2 being Element of I holds A /\ { w where w is Element of Omega : tau . w <= t2 } in MyFunc . t2 } by LOC1;

then consider B being Element of Sigma such that

GW1: ( A1 . n = B & ( for t2 being Element of I holds B /\ { w where w is Element of Omega : tau . w <= t2 } in MyFunc . t2 ) ) ;

reconsider A1n = A1 . n as Element of Sigma by GW1;

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

proof

(A1 . n) ` = (Complement A1) . n
by PROB_1:def 2;
let t be Element of I; :: thesis: ((A1 . n) `) /\ { 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;

E1: { w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) = ((A1 . n) `) /\ { 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 } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) is Event of MyFt2 by W2, PROB_1:24;

hence ((A1 . n) `) /\ { 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;

E1: { w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) = ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t }

proof

W2:
(A1 . n) /\ { w where w is Element of Omega : tau . w <= t } is Event of MyFt2
by GW1;
WW0:
for j being object st j in { w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) holds

j in ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t }

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

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

proof

for j being object st j in ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t } holds
let j be object ; :: thesis: ( j in { w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) implies j in ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t } )

assume h: j in { w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) ; :: thesis: j in ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t }

then Help0: j in { w where w is Element of Omega : tau . w <= t } ;

not j in (A1 . n) /\ { w where w is Element of Omega : tau . w <= t } by h, XBOOLE_0:def 5;

then Help2: not j in A1 . n by h, XBOOLE_0:def 4;

j in (A1 . n) `

end;assume h: j in { w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) ; :: thesis: j in ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t }

then Help0: j in { w where w is Element of Omega : tau . w <= t } ;

not j in (A1 . n) /\ { w where w is Element of Omega : tau . w <= t } by h, XBOOLE_0:def 5;

then Help2: not j in A1 . n by h, XBOOLE_0:def 4;

j in (A1 . n) `

proof

hence
j in ((A1 . n) `) /\ { 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 Help0;

hence j in (A1 . n) ` by XBOOLE_0:def 5, Help2; :: thesis: verum

end;( j = w2 & tau . w2 <= t ) by Help0;

hence j in (A1 . n) ` by XBOOLE_0:def 5, Help2; :: thesis: verum

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

proof

hence
{ w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) = ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t }
by WW0, TARSKI:2; :: thesis: verum
let j be object ; :: thesis: ( j in ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t } implies j in { w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) )

assume j in ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t } ; :: thesis: j in { w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } )

then j: ( j in Omega \ (A1 . n) & j in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 4;

then ( j in Omega & not j in A1 . n & j in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 5;

then not j in (A1 . n) /\ { 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 } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) by j, XBOOLE_0:def 5; :: thesis: verum

end;assume j in ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t } ; :: thesis: j in { w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } )

then j: ( j in Omega \ (A1 . n) & j in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 4;

then ( j in Omega & not j in A1 . n & j in { w where w is Element of Omega : tau . w <= t } ) by XBOOLE_0:def 5;

then not j in (A1 . n) /\ { 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 } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) by j, 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 } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) is Event of MyFt2 by W2, PROB_1:24;

hence ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t by E1; :: thesis: verum

hence ((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } is Element of El_Filtration (t,MyFunc) by GW2; :: thesis: verum