let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega st Omega = {1,2,3,4} holds
for MyFunc being Filtration of StoppingSet 2,Sigma st MyFunc . 0 = Special_SigmaField1 & MyFunc . 1 = Special_SigmaField2 & MyFunc . 2 = Trivial-SigmaField Omega holds
ex ST being Function of Omega,(StoppingSetExt 2) st
( ST is_StoppingTime_wrt MyFunc,2 & ST . 1 = 1 & ST . 2 = 1 & ST . 3 = 2 & ST . 4 = 2 & { w where w is Element of Omega : ST . w = 0 } = {} & { w where w is Element of Omega : ST . w = 1 } = {1,2} & { w where w is Element of Omega : ST . w = 2 } = {3,4} )
let Sigma be SigmaField of Omega; :: thesis: ( Omega = {1,2,3,4} implies for MyFunc being Filtration of StoppingSet 2,Sigma st MyFunc . 0 = Special_SigmaField1 & MyFunc . 1 = Special_SigmaField2 & MyFunc . 2 = Trivial-SigmaField Omega holds
ex ST being Function of Omega,(StoppingSetExt 2) st
( ST is_StoppingTime_wrt MyFunc,2 & ST . 1 = 1 & ST . 2 = 1 & ST . 3 = 2 & ST . 4 = 2 & { w where w is Element of Omega : ST . w = 0 } = {} & { w where w is Element of Omega : ST . w = 1 } = {1,2} & { w where w is Element of Omega : ST . w = 2 } = {3,4} ) )
assume ASS0: Omega = {1,2,3,4} ; :: thesis: for MyFunc being Filtration of StoppingSet 2,Sigma st MyFunc . 0 = Special_SigmaField1 & MyFunc . 1 = Special_SigmaField2 & MyFunc . 2 = Trivial-SigmaField Omega holds
ex ST being Function of Omega,(StoppingSetExt 2) st
( ST is_StoppingTime_wrt MyFunc,2 & ST . 1 = 1 & ST . 2 = 1 & ST . 3 = 2 & ST . 4 = 2 & { w where w is Element of Omega : ST . w = 0 } = {} & { w where w is Element of Omega : ST . w = 1 } = {1,2} & { w where w is Element of Omega : ST . w = 2 } = {3,4} )
let MyFunc be Filtration of StoppingSet 2,Sigma; :: thesis: ( MyFunc . 0 = Special_SigmaField1 & MyFunc . 1 = Special_SigmaField2 & MyFunc . 2 = Trivial-SigmaField Omega implies ex ST being Function of Omega,(StoppingSetExt 2) st
( ST is_StoppingTime_wrt MyFunc,2 & ST . 1 = 1 & ST . 2 = 1 & ST . 3 = 2 & ST . 4 = 2 & { w where w is Element of Omega : ST . w = 0 } = {} & { w where w is Element of Omega : ST . w = 1 } = {1,2} & { w where w is Element of Omega : ST . w = 2 } = {3,4} ) )
assume ASS2: ( MyFunc . 0 = Special_SigmaField1 & MyFunc . 1 = Special_SigmaField2 & MyFunc . 2 = Trivial-SigmaField Omega ) ; :: thesis: ex ST being Function of Omega,(StoppingSetExt 2) st
( ST is_StoppingTime_wrt MyFunc,2 & ST . 1 = 1 & ST . 2 = 1 & ST . 3 = 2 & ST . 4 = 2 & { w where w is Element of Omega : ST . w = 0 } = {} & { w where w is Element of Omega : ST . w = 1 } = {1,2} & { w where w is Element of Omega : ST . w = 2 } = {3,4} )
deffunc H₁( Element of Omega) -> Element of StoppingSetExt 2 = Special_StoppingSet $1;
consider f being Function of Omega,(StoppingSetExt 2) such that
A1: for d being Element of Omega holds f . d = H₁(d) from FUNCT_2:sch 4();
B1: ( 1 in {1,2} & 2 in {1,2} & not 3 in {1,2} & not 4 in {1,2} ) by TARSKI:def 2;
take f ; :: thesis: ( f is_StoppingTime_wrt MyFunc,2 & f . 1 = 1 & f . 2 = 1 & f . 3 = 2 & f . 4 = 2 & { w where w is Element of Omega : f . w = 0 } = {} & { w where w is Element of Omega : f . w = 1 } = {1,2} & { w where w is Element of Omega : f . w = 2 } = {3,4} )
A2: ( f . 1 = 1 & f . 2 = 1 & f . 3 = 2 & f . 4 = 2 )

proof

set O1 = 1;
set O2 = 2;
set O3 = 3;
set O4 = 4;
reconsider O1 = 1, O2 = 2, O3 = 3, O4 = 4 as Element of Omega by ASS0, ENUMSET1:def 2;
( f . 1 = H₁(O1) & f . 2 = H₁(O2) & f . 3 = H₁(O3) & f . 4 = H₁(O4) ) by A1;
hence ( f . 1 = 1 & f . 2 = 1 & f . 3 = 2 & f . 4 = 2 ) by B1, MATRIX_7:def 1; :: thesis: verum

end;

( f is_StoppingTime_wrt MyFunc,2 & { w where w is Element of Omega : f . w = 0 } = {} & { w where w is Element of Omega : f . w = 1 } = {1,2} & { w where w is Element of Omega : f . w = 2 } = {3,4} )

proof

G1: for t being Element of StoppingSet 2 holds
( { w where w is Element of Omega : f . w = t } in MyFunc . t & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) & ( t = 1 implies { w where w is Element of Omega : f . w = 1 } = {1,2} ) & ( t = 2 implies { w where w is Element of Omega : f . w = 2 } = {3,4} ) )

proof

let t be Element of StoppingSet 2; :: thesis: ( { w where w is Element of Omega : f . w = t } in MyFunc . t & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) & ( t = 1 implies { w where w is Element of Omega : f . w = 1 } = {1,2} ) & ( t = 2 implies { w where w is Element of Omega : f . w = 2 } = {3,4} ) )
t in StoppingSet 2 ;
then consider t1 being Element of NAT such that
H1: ( t = t1 & 0 <= t1 & t1 <= 2 ) ;
( t <= 1 or t = 1 + 1 ) by NAT_1:9, H1;
then g2: ( t <= 0 or t = 0 + 1 or t = 2 ) by NAT_1:9, H1;
( { w where w is Element of Omega : f . w = t } in MyFunc . t & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) & ( t = 1 implies { w where w is Element of Omega : f . w = 1 } = {1,2} ) & ( t = 2 implies { w where w is Element of Omega : f . w = 2 } = {3,4} ) )

proof

reconsider M = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;

per cases ( t = 0 or t = 1 or t = 2 ) by g2, H1;

suppose S1: t = 0 ; :: thesis: ( { w where w is Element of Omega : f . w = t } in MyFunc . t & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) & ( t = 1 implies { w where w is Element of Omega : f . w = 1 } = {1,2} ) & ( t = 2 implies { w where w is Element of Omega : f . w = 2 } = {3,4} ) )

( { w where w is Element of Omega : f . w = 0 } in M & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) )

proof

{ w where w is Element of Omega : f . w = 0 } c= {}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { w where w is Element of Omega : f . w = 0 } or y in {} )
assume y in { w where w is Element of Omega : f . w = 0 } ; :: thesis: y in {}
then ex y1 being Element of Omega st
( y = y1 & f . y1 = 0 ) ;
hence y in {} by A2, ASS0, ENUMSET1:def 2; :: thesis: verum

end;

then { w where w is Element of Omega : f . w = 0 } = {} ;
hence ( { w where w is Element of Omega : f . w = 0 } in M & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) ) by PROB_1:4; :: thesis: verum

end;

hence ( { w where w is Element of Omega : f . w = t } in MyFunc . t & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) & ( t = 1 implies { w where w is Element of Omega : f . w = 1 } = {1,2} ) & ( t = 2 implies { w where w is Element of Omega : f . w = 2 } = {3,4} ) ) by S1; :: thesis: verum

end;

suppose S1: t = 1 ; :: thesis: ( { w where w is Element of Omega : f . w = t } in MyFunc . t & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) & ( t = 1 implies { w where w is Element of Omega : f . w = 1 } = {1,2} ) & ( t = 2 implies { w where w is Element of Omega : f . w = 2 } = {3,4} ) )

{ w where w is Element of Omega : f . w = 1 } = {1,2}

proof

for x being object holds
( x in { w where w is Element of Omega : f . w = 1 } iff x in {1,2} )

proof

let x be object ; :: thesis: ( x in { w where w is Element of Omega : f . w = 1 } iff x in {1,2} )
thus ( x in { w where w is Element of Omega : f . w = 1 } implies x in {1,2} ) :: thesis: ( x in {1,2} implies x in { w where w is Element of Omega : f . w = 1 } )

proof

assume x in { w where w is Element of Omega : f . w = 1 } ; :: thesis: x in {1,2}
then consider w2 being Element of Omega such that
K2: ( x = w2 & f . w2 = 1 ) ;
( not w2 in {1,2} implies f . w2 > 1 )

proof

assume ASSJ: not w2 in {1,2} ; :: thesis: f . w2 > 1
( w2 = 1 or w2 = 2 or w2 = 3 or w2 = 4 ) by ASS0, ENUMSET1:def 2;
hence f . w2 > 1 by A2, ASSJ, TARSKI:def 2; :: thesis: verum

end;

hence x in {1,2} by K2; :: thesis: verum

end;

assume ASSJ: x in {1,2} ; :: thesis: x in { w where w is Element of Omega : f . w = 1 }
then ( x = 1 or x = 2 or x = 3 or x = 4 ) by TARSKI:def 2;
then S: x in Omega by ASS0, ENUMSET1:def 2;
( x = 1 or x = 2 ) by ASSJ, TARSKI:def 2;
hence x in { w where w is Element of Omega : f . w = 1 } by S, A2; :: thesis: verum

end;

hence { w where w is Element of Omega : f . w = 1 } = {1,2} by TARSKI:2; :: thesis: verum

end;

hence ( { w where w is Element of Omega : f . w = t } in MyFunc . t & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) & ( t = 1 implies { w where w is Element of Omega : f . w = 1 } = {1,2} ) & ( t = 2 implies { w where w is Element of Omega : f . w = 2 } = {3,4} ) ) by S1, ENUMSET1:def 2, ASS2; :: thesis: verum

end;

suppose S1: t = 2 ; :: thesis: ( { w where w is Element of Omega : f . w = t } in MyFunc . t & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) & ( t = 1 implies { w where w is Element of Omega : f . w = 1 } = {1,2} ) & ( t = 2 implies { w where w is Element of Omega : f . w = 2 } = {3,4} ) )

S2: { w where w is Element of Omega : f . w = t } = {3,4}

proof

for x being object holds
( x in { w where w is Element of Omega : f . w = t } iff x in {3,4} )

proof

let x be object ; :: thesis: ( x in { w where w is Element of Omega : f . w = t } iff x in {3,4} )
thus ( x in { w where w is Element of Omega : f . w = t } implies x in {3,4} ) :: thesis: ( x in {3,4} implies x in { w where w is Element of Omega : f . w = t } )

proof

assume x in { w where w is Element of Omega : f . w = t } ; :: thesis: x in {3,4}
then consider w2 being Element of Omega such that
K2: ( x = w2 & f . w2 = 2 ) by S1;
assume ASSJ: not x in {3,4} ; :: thesis: contradiction
( w2 = 1 or w2 = 2 or w2 = 3 or w2 = 4 ) by ASS0, ENUMSET1:def 2;
hence contradiction by A2, ASSJ, TARSKI:def 2, K2; :: thesis: verum

end;

assume x in {3,4} ; :: thesis: x in { w where w is Element of Omega : f . w = t }
then T: ( x = 3 or x = 4 ) by TARSKI:def 2;
then x in Omega by ASS0, ENUMSET1:def 2;
hence x in { w where w is Element of Omega : f . w = t } by A2, S1, T; :: thesis: verum

end;

hence { w where w is Element of Omega : f . w = t } = {3,4} by TARSKI:2; :: thesis: verum

end;

( {3,4} in Special_SigmaField2 & Special_SigmaField2 c= Trivial-SigmaField {1,2,3,4} ) by FINANCE3:24;
hence ( { w where w is Element of Omega : f . w = t } in MyFunc . t & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) & ( t = 1 implies { w where w is Element of Omega : f . w = 1 } = {1,2} ) & ( t = 2 implies { w where w is Element of Omega : f . w = 2 } = {3,4} ) ) by S2, S1, ASS2; :: thesis: verum

end;

end;

end;

hence ( { w where w is Element of Omega : f . w = t } in MyFunc . t & ( t = 0 implies { w where w is Element of Omega : f . w = 0 } = {} ) & ( t = 1 implies { w where w is Element of Omega : f . w = 1 } = {1,2} ) & ( t = 2 implies { w where w is Element of Omega : f . w = 2 } = {3,4} ) ) ; :: thesis: verum

end;

j1: 0 in StoppingSet 2 ;
j2: 1 in StoppingSet 2 ;
2 in StoppingSet 2 ;
hence ( f is_StoppingTime_wrt MyFunc,2 & { w where w is Element of Omega : f . w = 0 } = {} & { w where w is Element of Omega : f . w = 1 } = {1,2} & { w where w is Element of Omega : f . w = 2 } = {3,4} ) by j1, j2, G1; :: thesis: verum

end;

hence ( f is_StoppingTime_wrt MyFunc,2 & f . 1 = 1 & f . 2 = 1 & f . 3 = 2 & f . 4 = 2 & { w where w is Element of Omega : f . w = 0 } = {} & { w where w is Element of Omega : f . w = 1 } = {1,2} & { w where w is Element of Omega : f . w = 2 } = {3,4} ) by A2; :: thesis: verum