let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for T being Nat

for MyFunc being Filtration of StoppingSet T,Sigma

for k being Function of Omega,(StoppingSetExt T) holds

( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )

let Sigma be SigmaField of Omega; :: thesis: for T being Nat

for MyFunc being Filtration of StoppingSet T,Sigma

for k being Function of Omega,(StoppingSetExt T) holds

( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )

let T be Nat; :: thesis: for MyFunc being Filtration of StoppingSet T,Sigma

for k being Function of Omega,(StoppingSetExt T) holds

( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )

let MyFunc be Filtration of StoppingSet T,Sigma; :: thesis: for k being Function of Omega,(StoppingSetExt T) holds

( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )

let k be Function of Omega,(StoppingSetExt T); :: thesis: ( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )

thus ( k is_StoppingTime_wrt MyFunc,T implies for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t ) :: thesis: ( ( for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t ) implies k is_StoppingTime_wrt MyFunc,T )

for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w = t } in MyFunc . t

for T being Nat

for MyFunc being Filtration of StoppingSet T,Sigma

for k being Function of Omega,(StoppingSetExt T) holds

( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )

let Sigma be SigmaField of Omega; :: thesis: for T being Nat

for MyFunc being Filtration of StoppingSet T,Sigma

for k being Function of Omega,(StoppingSetExt T) holds

( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )

let T be Nat; :: thesis: for MyFunc being Filtration of StoppingSet T,Sigma

for k being Function of Omega,(StoppingSetExt T) holds

( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )

let MyFunc be Filtration of StoppingSet T,Sigma; :: thesis: for k being Function of Omega,(StoppingSetExt T) holds

( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )

let k be Function of Omega,(StoppingSetExt T); :: thesis: ( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )

thus ( k is_StoppingTime_wrt MyFunc,T implies for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t ) :: thesis: ( ( for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t ) implies k is_StoppingTime_wrt MyFunc,T )

proof

assume ASSJ1:
for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t
; :: thesis: k is_StoppingTime_wrt MyFunc,T
assume ASS:
k is_StoppingTime_wrt MyFunc,T
; :: thesis: for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t

for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t

end;for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t

proof

hence
for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t
; :: thesis: verum
defpred S_{1}[ Nat] means ( $1 in StoppingSet T implies { w where w is Element of Omega : k . w <= $1 } in MyFunc . $1 );

K1: { w where w is Element of Omega : k . w <= 0 } = { w where w is Element of Omega : k . w = 0 }_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(J0, J1);

for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t

end;K1: { w where w is Element of Omega : k . w <= 0 } = { w where w is Element of Omega : k . w = 0 }

proof

J0:
S
for q being object holds

( q in { w where w is Element of Omega : k . w <= 0 } iff q in { w where w is Element of Omega : k . w = 0 } )

end;( q in { w where w is Element of Omega : k . w <= 0 } iff q in { w where w is Element of Omega : k . w = 0 } )

proof

hence
{ w where w is Element of Omega : k . w <= 0 } = { w where w is Element of Omega : k . w = 0 }
by TARSKI:2; :: thesis: verum
let q be object ; :: thesis: ( q in { w where w is Element of Omega : k . w <= 0 } iff q in { w where w is Element of Omega : k . w = 0 } )

I1: ( ex q1 being Element of Omega st

( q = q1 & k . q1 <= 0 ) implies ex q2 being Element of Omega st

( q = q2 & k . q2 = 0 ) )

( q = q2 & k . q2 = 0 ) implies ex q1 being Element of Omega st

( q = q1 & k . q1 <= 0 ) ) ;

hence ( q in { w where w is Element of Omega : k . w <= 0 } iff q in { w where w is Element of Omega : k . w = 0 } ) by I1; :: thesis: verum

end;I1: ( ex q1 being Element of Omega st

( q = q1 & k . q1 <= 0 ) implies ex q2 being Element of Omega st

( q = q2 & k . q2 = 0 ) )

proof

( ex q2 being Element of Omega st
given q2 being Element of Omega such that II:
( q = q2 & k . q2 <= 0 )
; :: thesis: ex q2 being Element of Omega st

( q = q2 & k . q2 = 0 )

k . q2 = 0

( q = q2 & k . q2 = 0 ) by II; :: thesis: verum

end;( q = q2 & k . q2 = 0 )

k . q2 = 0

proof
end;

hence
ex q2 being Element of Omega st ( q = q2 & k . q2 = 0 ) by II; :: thesis: verum

( q = q2 & k . q2 = 0 ) implies ex q1 being Element of Omega st

( q = q1 & k . q1 <= 0 ) ) ;

hence ( q in { w where w is Element of Omega : k . w <= 0 } iff q in { w where w is Element of Omega : k . w = 0 } ) by I1; :: thesis: verum

proof

J1:
for n being Nat st S
{ w where w is Element of Omega : k . w <= 0 } in MyFunc . 0
_{1}[ 0 ]
; :: thesis: verum

end;proof

hence
S
0 in StoppingSet T
;

hence { w where w is Element of Omega : k . w <= 0 } in MyFunc . 0 by K1, ASS; :: thesis: verum

end;hence { w where w is Element of Omega : k . w <= 0 } in MyFunc . 0 by K1, ASS; :: thesis: verum

S

proof

Q1:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume j1: S_{1}[n]
; :: thesis: S_{1}[n + 1]

( n + 1 in StoppingSet T implies { w where w is Element of Omega : k . w <= n + 1 } in MyFunc . (n + 1) )_{1}[n + 1]
; :: thesis: verum

end;assume j1: S

( n + 1 in StoppingSet T implies { w where w is Element of Omega : k . w <= n + 1 } in MyFunc . (n + 1) )

proof

hence
S
assume ASSJ10:
n + 1 in StoppingSet T
; :: thesis: { w where w is Element of Omega : k . w <= n + 1 } in MyFunc . (n + 1)

J10: { w where w is Element of Omega : k . w <= n + 1 } = { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 }

{ w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } in MyFunc . (n + 1)

end;J10: { w where w is Element of Omega : k . w <= n + 1 } = { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 }

proof

reconsider n = n as Element of NAT by ORDINAL1:def 12;
for x being object holds

( x in { w where w is Element of Omega : k . w <= n + 1 } iff x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } )

end;( x in { w where w is Element of Omega : k . w <= n + 1 } iff x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } )

proof

hence
{ w where w is Element of Omega : k . w <= n + 1 } = { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 }
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in { w where w is Element of Omega : k . w <= n + 1 } iff x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } )

thus ( x in { w where w is Element of Omega : k . w <= n + 1 } implies x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } ) :: thesis: ( x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } implies x in { w where w is Element of Omega : k . w <= n + 1 } )

end;thus ( x in { w where w is Element of Omega : k . w <= n + 1 } implies x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } ) :: thesis: ( x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } implies x in { w where w is Element of Omega : k . w <= n + 1 } )

proof

assume
x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 }
; :: thesis: x in { w where w is Element of Omega : k . w <= n + 1 }
assume
x in { w where w is Element of Omega : k . w <= n + 1 }
; :: thesis: x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 }

then consider w being Element of Omega such that

XX: ( x = w & k . w <= n + 1 ) ;

set KW = k . w;

end;then consider w being Element of Omega such that

XX: ( x = w & k . w <= n + 1 ) ;

set KW = k . w;

per cases
( ( x = w & k . w <= n ) or ( x = w & not k . w <= n ) )
by XX;

end;

suppose
( x = w & k . w <= n )
; :: thesis: x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 }

then
x in { w where w is Element of Omega : k . w <= n }
;

hence x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } by XBOOLE_0:def 3; :: thesis: verum

end;hence x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } by XBOOLE_0:def 3; :: thesis: verum

suppose S1:
( x = w & not k . w <= n )
; :: thesis: x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 }

k . w = n + 1

hence x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } by XBOOLE_0:def 3; :: thesis: verum

end;proof

then
x in { w where w is Element of Omega : k . w = n + 1 }
by XX;
( k . w is Element of NAT or k . w = +infty )

end;proof

then reconsider KW = k . w as Element of NAT by NUMBERS:19, XX, XXREAL_0:9;
( k . w in StoppingSet T or k . w in {+infty} )
by XBOOLE_0:def 3;

end;hence x in { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } by XBOOLE_0:def 3; :: thesis: verum

per cases then
( x in { w where w is Element of Omega : k . w <= n } or x in { w where w is Element of Omega : k . w = n + 1 } )
by XBOOLE_0:def 3;

end;

suppose JP:
x in { w where w is Element of Omega : k . w <= n }
; :: thesis: x in { w where w is Element of Omega : k . w <= n + 1 }

x in { w where w is Element of Omega : k . w <= n + 1 }

end;proof

hence
x in { w where w is Element of Omega : k . w <= n + 1 }
; :: thesis: verum
consider q being Element of Omega such that

Q1: ( x = q & k . q <= n ) by JP;

set KJ = k . q;

( k . q is Element of NAT or k . q = +infty )

( KJ <= n implies KJ <= n + 1 ) by NAT_1:12;

hence x in { w where w is Element of Omega : k . w <= n + 1 } by Q1; :: thesis: verum

end;Q1: ( x = q & k . q <= n ) by JP;

set KJ = k . q;

( k . q is Element of NAT or k . q = +infty )

proof

then reconsider KJ = k . q as Element of NAT by XREAL_0:def 1, Q1, XXREAL_0:9;
( k . q in StoppingSet T or k . q in {+infty} )
by XBOOLE_0:def 3;

end;( KJ <= n implies KJ <= n + 1 ) by NAT_1:12;

hence x in { w where w is Element of Omega : k . w <= n + 1 } by Q1; :: thesis: verum

suppose JP:
x in { w where w is Element of Omega : k . w = n + 1 }
; :: thesis: x in { w where w is Element of Omega : k . w <= n + 1 }

x in { w where w is Element of Omega : k . w <= n + 1 }

end;proof

hence
x in { w where w is Element of Omega : k . w <= n + 1 }
; :: thesis: verum
ex q being Element of Omega st

( x = q & k . q = n + 1 ) by JP;

hence x in { w where w is Element of Omega : k . w <= n + 1 } ; :: thesis: verum

end;( x = q & k . q = n + 1 ) by JP;

hence x in { w where w is Element of Omega : k . w <= n + 1 } ; :: thesis: verum

{ w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } in MyFunc . (n + 1)

proof

hence
{ w where w is Element of Omega : k . w <= n + 1 } in MyFunc . (n + 1)
by J10; :: thesis: verum
set A = { w where w is Element of Omega : k . w <= n } ;

set B = { w where w is Element of Omega : k . w = n + 1 } ;

set C = MyFunc . (n + 1);

reconsider C = MyFunc . (n + 1) as SigmaField of Omega by ASSJ10, KOLMOG01:def 2;

n in StoppingSet T

h2: { w where w is Element of Omega : k . w <= n } is Element of C

then { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } is Event of C by h2, PROB_1:21;

hence { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } in MyFunc . (n + 1) ; :: thesis: verum

end;set B = { w where w is Element of Omega : k . w = n + 1 } ;

set C = MyFunc . (n + 1);

reconsider C = MyFunc . (n + 1) as SigmaField of Omega by ASSJ10, KOLMOG01:def 2;

n in StoppingSet T

proof

then reconsider n = n as Element of StoppingSet T ;
consider t being Element of NAT such that

Y20: ( n + 1 = t & 0 <= t & t <= T ) by ASSJ10;

( 0 <= n & n <= T ) by Y20, NAT_1:13;

hence n in StoppingSet T ; :: thesis: verum

end;Y20: ( n + 1 = t & 0 <= t & t <= T ) by ASSJ10;

( 0 <= n & n <= T ) by Y20, NAT_1:13;

hence n in StoppingSet T ; :: thesis: verum

h2: { w where w is Element of Omega : k . w <= n } is Element of C

proof

{ w where w is Element of Omega : k . w = n + 1 } is Event of C
by ASSJ10, ASS;
for x being set st x in MyFunc . n holds

x in MyFunc . (n + 1)

end;x in MyFunc . (n + 1)

proof

hence
{ w where w is Element of Omega : k . w <= n } is Element of C
by j1; :: thesis: verum
MyFunc . n is Subset of (MyFunc . (n + 1))
by FINANCE3:def 9, NAT_1:12, ASSJ10;

hence for x being set st x in MyFunc . n holds

x in MyFunc . (n + 1) ; :: thesis: verum

end;hence for x being set st x in MyFunc . n holds

x in MyFunc . (n + 1) ; :: thesis: verum

then { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } is Event of C by h2, PROB_1:21;

hence { w where w is Element of Omega : k . w <= n } \/ { w where w is Element of Omega : k . w = n + 1 } in MyFunc . (n + 1) ; :: thesis: verum

for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t

proof

hence
for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t
; :: thesis: verum
let t be Element of StoppingSet T; :: thesis: { w where w is Element of Omega : k . w <= t } in MyFunc . t

t in StoppingSet T ;

then ex s being Element of NAT st

( t = s & 0 <= s & s <= T ) ;

hence { w where w is Element of Omega : k . w <= t } in MyFunc . t by Q1; :: thesis: verum

end;t in StoppingSet T ;

then ex s being Element of NAT st

( t = s & 0 <= s & s <= T ) ;

hence { w where w is Element of Omega : k . w <= t } in MyFunc . t by Q1; :: thesis: verum

for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w = t } in MyFunc . t

proof

hence
k is_StoppingTime_wrt MyFunc,T
; :: thesis: verum
let t be Element of StoppingSet T; :: thesis: { w where w is Element of Omega : k . w = t } in MyFunc . t

defpred S_{1}[ Nat] means ( $1 + 1 in StoppingSet T implies { w where w is Element of Omega : k . w < $1 + 1 } in MyFunc . ($1 + 1) );

J01: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(J01, J11);

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

QH1: { w where w is Element of Omega : k . w <= t } is Element of M by ASSJ1;

t in StoppingSet T ;

then consider q being Element of NAT such that

QH3: ( t = q & 0 <= q & q <= T ) ;

reconsider t = t as Nat by QH3;

Q2: { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } is Event of M

end;defpred S

J01: S

proof

J11:
for n being Nat st S
( 0 + 1 in StoppingSet T implies { w where w is Element of Omega : k . w < 0 + 1 } in MyFunc . (0 + 1) )
_{1}[ 0 ]
; :: thesis: verum

end;proof

hence
S
assume ASS:
0 + 1 in StoppingSet T
; :: thesis: { w where w is Element of Omega : k . w < 0 + 1 } in MyFunc . (0 + 1)

{ w where w is Element of Omega : k . w < 0 + 1 } in MyFunc . (0 + 1)

end;{ w where w is Element of Omega : k . w < 0 + 1 } in MyFunc . (0 + 1)

proof

hence
{ w where w is Element of Omega : k . w < 0 + 1 } in MyFunc . (0 + 1)
; :: thesis: verum
H1:
{ w where w is Element of Omega : k . w <= 0 } = { w where w is Element of Omega : k . w < 0 + 1 }

then reconsider JA = 0 as Element of StoppingSet T ;

reconsider JB = 0 + 1 as Element of StoppingSet T by ASS;

h2: MyFunc . JA is Subset of (MyFunc . JB) by FINANCE3:def 9;

{ w where w is Element of Omega : k . w <= 0 } in MyFunc . 0 by ASSJ1, T1;

hence { w where w is Element of Omega : k . w < 0 + 1 } in MyFunc . (0 + 1) by H1, h2; :: thesis: verum

end;proof

T1:
0 in StoppingSet T
;
for x being object holds

( x in { w where w is Element of Omega : k . w <= 0 } iff x in { w where w is Element of Omega : k . w < 0 + 1 } )

end;( x in { w where w is Element of Omega : k . w <= 0 } iff x in { w where w is Element of Omega : k . w < 0 + 1 } )

proof

hence
{ w where w is Element of Omega : k . w <= 0 } = { w where w is Element of Omega : k . w < 0 + 1 }
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in { w where w is Element of Omega : k . w <= 0 } iff x in { w where w is Element of Omega : k . w < 0 + 1 } )

thus ( x in { w where w is Element of Omega : k . w <= 0 } implies x in { w where w is Element of Omega : k . w < 0 + 1 } ) :: thesis: ( x in { w where w is Element of Omega : k . w < 0 + 1 } implies x in { w where w is Element of Omega : k . w <= 0 } )

then consider w1 being Element of Omega such that

W1: ( x = w1 & k . w1 < 0 + 1 ) ;

set KWJ = k . w1;

( k . w1 is Element of NAT or k . w1 = +infty )

KWJ <= 0 by NAT_1:13, W1;

hence x in { w where w is Element of Omega : k . w <= 0 } by W1; :: thesis: verum

end;thus ( x in { w where w is Element of Omega : k . w <= 0 } implies x in { w where w is Element of Omega : k . w < 0 + 1 } ) :: thesis: ( x in { w where w is Element of Omega : k . w < 0 + 1 } implies x in { w where w is Element of Omega : k . w <= 0 } )

proof

assume
x in { w where w is Element of Omega : k . w < 0 + 1 }
; :: thesis: x in { w where w is Element of Omega : k . w <= 0 }
assume
x in { w where w is Element of Omega : k . w <= 0 }
; :: thesis: x in { w where w is Element of Omega : k . w < 0 + 1 }

then consider w1 being Element of Omega such that

W1: ( x = w1 & k . w1 <= 0 ) ;

thus x in { w where w is Element of Omega : k . w < 0 + 1 } by W1; :: thesis: verum

end;then consider w1 being Element of Omega such that

W1: ( x = w1 & k . w1 <= 0 ) ;

thus x in { w where w is Element of Omega : k . w < 0 + 1 } by W1; :: thesis: verum

then consider w1 being Element of Omega such that

W1: ( x = w1 & k . w1 < 0 + 1 ) ;

set KWJ = k . w1;

( k . w1 is Element of NAT or k . w1 = +infty )

proof

then reconsider KWJ = k . w1 as Nat by NUMBERS:19, W1, XXREAL_0:9;
( k . w1 in StoppingSet T or k . w1 in {+infty} )
by XBOOLE_0:def 3;

end;KWJ <= 0 by NAT_1:13, W1;

hence x in { w where w is Element of Omega : k . w <= 0 } by W1; :: thesis: verum

then reconsider JA = 0 as Element of StoppingSet T ;

reconsider JB = 0 + 1 as Element of StoppingSet T by ASS;

h2: MyFunc . JA is Subset of (MyFunc . JB) by FINANCE3:def 9;

{ w where w is Element of Omega : k . w <= 0 } in MyFunc . 0 by ASSJ1, T1;

hence { w where w is Element of Omega : k . w < 0 + 1 } in MyFunc . (0 + 1) by H1, h2; :: thesis: verum

S

proof

Q1:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume S_{1}[n]
; :: thesis: S_{1}[n + 1]

( (n + 1) + 1 in StoppingSet T implies { w where w is Element of Omega : k . w < (n + 1) + 1 } in MyFunc . ((n + 1) + 1) )_{1}[n + 1]
; :: thesis: verum

end;assume S

( (n + 1) + 1 in StoppingSet T implies { w where w is Element of Omega : k . w < (n + 1) + 1 } in MyFunc . ((n + 1) + 1) )

proof

hence
S
assume N01:
(n + 1) + 1 in StoppingSet T
; :: thesis: { w where w is Element of Omega : k . w < (n + 1) + 1 } in MyFunc . ((n + 1) + 1)

M10: { w where w is Element of Omega : k . w < (n + 1) + 1 } = { w where w is Element of Omega : k . w <= n + 1 }

then MyFunc . (n + 1) is Subset of (MyFunc . ((n + 1) + 1)) by FINANCE3:def 9, N01;

then MyFunc . (n + 1) c= MyFunc . ((n + 1) + 1) ;

hence { w where w is Element of Omega : k . w < (n + 1) + 1 } in MyFunc . ((n + 1) + 1) by M10, ASSJ1, s1; :: thesis: verum

end;M10: { w where w is Element of Omega : k . w < (n + 1) + 1 } = { w where w is Element of Omega : k . w <= n + 1 }

proof

s1:
n + 1 in StoppingSet T
for x being object holds

( x in { w where w is Element of Omega : k . w < (n + 1) + 1 } iff x in { w where w is Element of Omega : k . w <= n + 1 } )

end;( x in { w where w is Element of Omega : k . w < (n + 1) + 1 } iff x in { w where w is Element of Omega : k . w <= n + 1 } )

proof

hence
{ w where w is Element of Omega : k . w < (n + 1) + 1 } = { w where w is Element of Omega : k . w <= n + 1 }
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in { w where w is Element of Omega : k . w < (n + 1) + 1 } iff x in { w where w is Element of Omega : k . w <= n + 1 } )

thus ( x in { w where w is Element of Omega : k . w < (n + 1) + 1 } implies x in { w where w is Element of Omega : k . w <= n + 1 } ) :: thesis: ( x in { w where w is Element of Omega : k . w <= n + 1 } implies x in { w where w is Element of Omega : k . w < (n + 1) + 1 } )

then consider w3 being Element of Omega such that

QZ1: ( x = w3 & k . w3 <= n + 1 ) ;

set KW = k . w3;

k . w3 in StoppingSet T

L21: ( k . w3 = w2 & 0 <= w2 & w2 <= T ) ;

k . w3 < (n + 1) + 1 by QZ1, NAT_1:13, L21;

hence x in { w where w is Element of Omega : k . w < (n + 1) + 1 } by QZ1; :: thesis: verum

end;thus ( x in { w where w is Element of Omega : k . w < (n + 1) + 1 } implies x in { w where w is Element of Omega : k . w <= n + 1 } ) :: thesis: ( x in { w where w is Element of Omega : k . w <= n + 1 } implies x in { w where w is Element of Omega : k . w < (n + 1) + 1 } )

proof

assume
x in { w where w is Element of Omega : k . w <= n + 1 }
; :: thesis: x in { w where w is Element of Omega : k . w < (n + 1) + 1 }
assume
x in { w where w is Element of Omega : k . w < (n + 1) + 1 }
; :: thesis: x in { w where w is Element of Omega : k . w <= n + 1 }

then consider w being Element of Omega such that

F11: ( x = w & k . w < (n + 1) + 1 ) ;

set KW = k . w;

a1: k . w in StoppingSet T

L21: ( k . w = w2 & 0 <= w2 & w2 <= T ) by a1;

( k . w < (n + 1) + 1 iff k . w <= n + 1 ) by NAT_1:13, L21;

hence x in { w where w is Element of Omega : k . w <= n + 1 } by F11; :: thesis: verum

end;then consider w being Element of Omega such that

F11: ( x = w & k . w < (n + 1) + 1 ) ;

set KW = k . w;

a1: k . w in StoppingSet T

proof

consider w2 being Element of NAT such that
(n + 1) + 1 in REAL
by NUMBERS:19;

then k . w < +infty by F11, XXREAL_0:2, XXREAL_0:9;

then not k . w in {+infty} by TARSKI:def 1;

hence k . w in StoppingSet T by XBOOLE_0:def 3; :: thesis: verum

end;then k . w < +infty by F11, XXREAL_0:2, XXREAL_0:9;

then not k . w in {+infty} by TARSKI:def 1;

hence k . w in StoppingSet T by XBOOLE_0:def 3; :: thesis: verum

L21: ( k . w = w2 & 0 <= w2 & w2 <= T ) by a1;

( k . w < (n + 1) + 1 iff k . w <= n + 1 ) by NAT_1:13, L21;

hence x in { w where w is Element of Omega : k . w <= n + 1 } by F11; :: thesis: verum

then consider w3 being Element of Omega such that

QZ1: ( x = w3 & k . w3 <= n + 1 ) ;

set KW = k . w3;

k . w3 in StoppingSet T

proof

then consider w2 being Element of NAT such that
not k . w3 in {+infty}

end;proof

hence
k . w3 in StoppingSet T
by XBOOLE_0:def 3; :: thesis: verum
n + 1 < +infty
by XXREAL_0:9, NUMBERS:19;

hence not k . w3 in {+infty} by TARSKI:def 1, QZ1; :: thesis: verum

end;hence not k . w3 in {+infty} by TARSKI:def 1, QZ1; :: thesis: verum

L21: ( k . w3 = w2 & 0 <= w2 & w2 <= T ) ;

k . w3 < (n + 1) + 1 by QZ1, NAT_1:13, L21;

hence x in { w where w is Element of Omega : k . w < (n + 1) + 1 } by QZ1; :: thesis: verum

proof

( n + 1 in StoppingSet T & n + 1 <= (n + 1) + 1 )
by NAT_1:13, s1;
consider w3 being Element of NAT such that

QZ10: ( w3 = (n + 1) + 1 & 0 <= w3 & w3 <= T ) by N01;

n + 1 < T by NAT_1:13, QZ10;

hence n + 1 in StoppingSet T ; :: thesis: verum

end;QZ10: ( w3 = (n + 1) + 1 & 0 <= w3 & w3 <= T ) by N01;

n + 1 < T by NAT_1:13, QZ10;

hence n + 1 in StoppingSet T ; :: thesis: verum

then MyFunc . (n + 1) is Subset of (MyFunc . ((n + 1) + 1)) by FINANCE3:def 9, N01;

then MyFunc . (n + 1) c= MyFunc . ((n + 1) + 1) ;

hence { w where w is Element of Omega : k . w < (n + 1) + 1 } in MyFunc . ((n + 1) + 1) by M10, ASSJ1, s1; :: thesis: verum

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

QH1: { w where w is Element of Omega : k . w <= t } is Element of M by ASSJ1;

t in StoppingSet T ;

then consider q being Element of NAT such that

QH3: ( t = q & 0 <= q & q <= T ) ;

reconsider t = t as Nat by QH3;

Q2: { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } is Event of M

proof

{ w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } = { w where w is Element of Omega : k . w = t }
{ w where w is Element of Omega : k . w < t } is Element of M

end;proof
end;

hence
{ w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } is Event of M
by QH1, PROB_1:24; :: thesis: verumper cases
( t = 0 or t > 0 )
;

end;

suppose S1:
t = 0
; :: thesis: { w where w is Element of Omega : k . w < t } is Element of M

s2:
{ w where w is Element of Omega : k . w < 0 } c= {}

{} is Element of M by PROB_1:22;

hence { w where w is Element of Omega : k . w < t } is Element of M by s2, S1; :: thesis: verum

end;proof

reconsider M = M as SigmaField of Omega ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of Omega : k . w < 0 } or x in {} )

assume x in { w where w is Element of Omega : k . w < 0 } ; :: thesis: x in {}

then consider w being Element of Omega such that

TT: ( x = w & k . w < 0 ) ;

k . w >= 0

end;assume x in { w where w is Element of Omega : k . w < 0 } ; :: thesis: x in {}

then consider w being Element of Omega such that

TT: ( x = w & k . w < 0 ) ;

k . w >= 0

proof

hence
x in {}
by TT; :: thesis: verum
( k . w in StoppingSet T or k . w in {+infty} )
by XBOOLE_0:def 3;

end;{} is Element of M by PROB_1:22;

hence { w where w is Element of Omega : k . w < t } is Element of M by s2, S1; :: thesis: verum

proof

hence
{ w where w is Element of Omega : k . w = t } in MyFunc . t
by Q2; :: thesis: verum
for x being object holds

( x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } iff x in { w where w is Element of Omega : k . w = t } )

end;( x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } iff x in { w where w is Element of Omega : k . w = t } )

proof

hence
{ w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } = { w where w is Element of Omega : k . w = t }
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } iff x in { w where w is Element of Omega : k . w = t } )

thus ( x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } implies x in { w where w is Element of Omega : k . w = t } ) :: thesis: ( x in { w where w is Element of Omega : k . w = t } implies x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } )

then consider w being Element of Omega such that

W1: ( x = w & k . w = t ) ;

( ex w1 being Element of Omega st

( x = w1 & k . w1 <= t ) & ( for w1 being Element of Omega holds

( not x = w1 or not k . w1 < t ) ) ) by W1;

then ( x in { w where w is Element of Omega : k . w <= t } & not x in { w where w is Element of Omega : k . w < t } ) ;

hence x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } by XBOOLE_0:def 5; :: thesis: verum

end;thus ( x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } implies x in { w where w is Element of Omega : k . w = t } ) :: thesis: ( x in { w where w is Element of Omega : k . w = t } implies x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } )

proof

assume
x in { w where w is Element of Omega : k . w = t }
; :: thesis: x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t }
assume
x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t }
; :: thesis: x in { w where w is Element of Omega : k . w = t }

then JJJ: ( x in { w where w is Element of Omega : k . w <= t } & not x in { w where w is Element of Omega : k . w < t } ) by XBOOLE_0:def 5;

then consider w1 being Element of Omega such that

JJJ1: ( w1 = x & k . w1 <= t ) ;

w1 in { w where w is Element of Omega : k . w = t }

end;then JJJ: ( x in { w where w is Element of Omega : k . w <= t } & not x in { w where w is Element of Omega : k . w < t } ) by XBOOLE_0:def 5;

then consider w1 being Element of Omega such that

JJJ1: ( w1 = x & k . w1 <= t ) ;

w1 in { w where w is Element of Omega : k . w = t }

proof

hence
x in { w where w is Element of Omega : k . w = t }
by JJJ1; :: thesis: verum
( k . w1 <= t & k . w1 >= t implies k . w1 = t )

end;proof

hence
w1 in { w where w is Element of Omega : k . w = t }
by JJJ1, JJJ; :: thesis: verum
assume Q0:
( k . w1 <= t & k . w1 >= t )
; :: thesis: k . w1 = t

set W = k . w1;

( k . w1 in StoppingSet T or k . w1 in {+infty} ) by XBOOLE_0:def 3;

then ( ex w3 being Element of NAT st

( w3 = k . w1 & 0 <= w3 & w3 <= T ) or k . w1 = +infty ) by TARSKI:def 1;

then reconsider W = k . w1 as Nat by JJJ1, XXREAL_0:9;

W + 1 > t by NAT_1:13, Q0;

hence k . w1 = t by Q0, NAT_1:22; :: thesis: verum

end;set W = k . w1;

( k . w1 in StoppingSet T or k . w1 in {+infty} ) by XBOOLE_0:def 3;

then ( ex w3 being Element of NAT st

( w3 = k . w1 & 0 <= w3 & w3 <= T ) or k . w1 = +infty ) by TARSKI:def 1;

then reconsider W = k . w1 as Nat by JJJ1, XXREAL_0:9;

W + 1 > t by NAT_1:13, Q0;

hence k . w1 = t by Q0, NAT_1:22; :: thesis: verum

then consider w being Element of Omega such that

W1: ( x = w & k . w = t ) ;

( ex w1 being Element of Omega st

( x = w1 & k . w1 <= t ) & ( for w1 being Element of Omega holds

( not x = w1 or not k . w1 < t ) ) ) by W1;

then ( x in { w where w is Element of Omega : k . w <= t } & not x in { w where w is Element of Omega : k . w < t } ) ;

hence x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } by XBOOLE_0:def 5; :: thesis: verum