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
proof
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 }
proof
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 }
proof
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) `
proof
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;
hence j in ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t } by XBOOLE_0:def 4, h; :: thesis: verum
end;
for j being object st j in ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t } holds
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
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;
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
end;
W2: (A1 . n) /\ { 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 } \ ((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;
(A1 . n) ` = (Complement A1) . n by PROB_1:def 2;
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