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_{1}( 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_{1}(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 )

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

consider f being Function of Omega,(StoppingSetExt 2) such that

A1: for d being Element of Omega holds f . d = H

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

( 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} )
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_{1}(O1) & f . 2 = H_{1}(O2) & f . 3 = H_{1}(O3) & f . 4 = H_{1}(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;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

hence ( f . 1 = 1 & f . 2 = 1 & f . 3 = 2 & f . 4 = 2 ) by B1, MATRIX_7:def 1; :: thesis: verum

proof

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

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

j1:
0 in StoppingSet 2
;
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} ) )

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

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
reconsider M = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;

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

end;

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 } = {} ) )

end;proof

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
{ w where w is Element of Omega : f . w = 0 } c= {}

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

then
{ w where w is Element of Omega : f . w = 0 } = {}
;
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;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

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

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}

end;proof

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
for x being object holds

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

end;( x in { w where w is Element of Omega : f . w = 1 } iff x in {1,2} )

proof

hence
{ w where w is Element of Omega : f . w = 1 } = {1,2}
by TARSKI:2; :: thesis: verum
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 } )

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;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 ASSJ:
x in {1,2}
; :: thesis: x in { w where w is Element of Omega : f . w = 1 }
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 )

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

hence
x in {1,2}
by K2; :: thesis: verum
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;( 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

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

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}

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

( {3,4} in Special_SigmaField2 & Special_SigmaField2 c= Trivial-SigmaField {1,2,3,4} )
by FINANCE3:24;
for x being object holds

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

end;( x in { w where w is Element of Omega : f . w = t } iff x in {3,4} )

proof

hence
{ w where w is Element of Omega : f . w = t } = {3,4}
by TARSKI:2; :: thesis: verum
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 } )

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;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 {3,4}
; :: thesis: x in { w where w is Element of Omega : f . w = t }
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;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

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

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

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