let Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let T be Nat; :: thesis:
let MyFunc be Filtration of StoppingSet T,Sigma; :: thesis:
let k be Function of Omega,(StoppingSetExt T); :: thesis:
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:

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

defpred S₁[ 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 }

proof

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

proof

let q be object ; :: thesis:
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

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

proof

per cases by XBOOLE_0:def 3;

suppose k . q2 in StoppingSet T ; :: thesis:

then ex s being Element of NAT st
( k . q2 = s & 0 <= s & s <= T ) ;
hence k . q2 = 0 by II; :: thesis:

end;

suppose k . q2 in {+infty} ; :: thesis:

hence k . q2 = 0 by II, TARSKI:def 1; :: thesis:

end;

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

end;

( ex q2 being Element of Omega st
( 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:

end;

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:

end;

J0: S₁[ 0 ]

proof

{ w where w is Element of Omega : k . w <= 0 } in MyFunc . 0

proof

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

end;

hence S₁[ 0 ] ; :: thesis:

end;

J1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume j1: S₁[n] ; :: thesis:
( n + 1 in StoppingSet T implies { w where w is Element of Omega : k . w <= n + 1 } in MyFunc . (n + 1) )

proof

assume ASSJ10: n + 1 in StoppingSet T ; :: thesis:
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

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

proof

let x be object ; :: thesis:
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:

proof

assume x in { w where w is Element of Omega : k . w <= n + 1 } ; :: thesis:
then consider w being Element of Omega such that
XX: ( x = w & k . w <= n + 1 ) ;
set KW = k . w;

per cases by XX;

suppose ( x = w & k . w <= n ) ; :: thesis:

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:

end;

suppose S1: ( x = w & not k . w <= n ) ; :: thesis:

k . w = n + 1

proof

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

proof

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

per cases by TARSKI:def 1;

suppose k . w = +infty ; :: thesis:

hence ( k . w is Element of NAT or k . w = +infty ) ; :: thesis:

end;

suppose k . w in StoppingSet T ; :: thesis:

then ex q being Element of NAT st
( k . w = q & 0 <= q & q <= T ) ;
hence ( k . w is Element of NAT or k . w = +infty ) ; :: thesis:

end;

then reconsider KW = k . w as Element of NAT by NUMBERS:19, XX, XXREAL_0:9;

per cases by XX, NAT_1:8;

suppose KW <= n ; :: thesis:

hence k . w = n + 1 by S1; :: thesis:

end;

suppose KW = n + 1 ; :: thesis:

hence k . w = n + 1 ; :: thesis:

end;

then x in { w where w is Element of Omega : k . w = n + 1 } by XX;
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:

end;

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:

per cases by XBOOLE_0:def 3;

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 }

proof

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 )

proof

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

per cases by TARSKI:def 1;

suppose k . q = +infty ; :: thesis:

hence ( k . q is Element of NAT or k . q = +infty ) ; :: thesis:

end;

suppose k . q in StoppingSet T ; :: thesis:

then ex q1 being Element of NAT st
( k . q = q1 & 0 <= q1 & q1 <= T ) ;
hence ( k . q is Element of NAT or k . q = +infty ) ; :: thesis:

end;

then reconsider KJ = k . q as Element of NAT by XREAL_0:def 1, Q1, XXREAL_0:9;
( 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:

end;

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

end;

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 }

proof

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:

end;

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

end;

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:

end;

reconsider n = n as Element of NAT by ORDINAL1:def 12;
{ 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

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

proof

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:

end;

then reconsider n = n as Element of StoppingSet T ;
h2: { w where w is Element of Omega : k . w <= n } is Element of C

proof

for x being set st x in MyFunc . n holds
x in MyFunc . (n + 1)

proof

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:

end;

hence { w where w is Element of Omega : k . w <= n } is Element of C by j1; :: thesis:

end;

{ w where w is Element of Omega : k . w = n + 1 } is Event of C by ASSJ10, ASS;
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:

end;

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

end;

hence S₁[n + 1] ; :: thesis:

end;

Q1: for n being Nat holds S₁[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

proof

let t be Element of StoppingSet T; :: thesis:
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:

end;

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

end;

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

end;

assume ASSJ1: 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

proof

let t be Element of StoppingSet T; :: thesis:
defpred S₁[ 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₁[ 0 ]

proof

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

proof

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

proof

H1: { w where w is Element of Omega : k . w <= 0 } = { w where w is Element of Omega : k . w < 0 + 1 }

proof

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

proof

let x be object ; :: thesis:
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:

proof

assume x in { w where w is Element of Omega : k . w <= 0 } ; :: thesis:
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:

end;

assume x in { w where w is Element of Omega : k . w < 0 + 1 } ; :: thesis:
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

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

per cases by TARSKI:def 1;

suppose k . w1 = +infty ; :: thesis:

hence ( k . w1 is Element of NAT or k . w1 = +infty ) ; :: thesis:

end;

suppose k . w1 in StoppingSet T ; :: thesis:

then ex q1 being Element of NAT st
( k . w1 = q1 & 0 <= q1 & q1 <= T ) ;
hence ( k . w1 is Element of NAT or k . w1 = +infty ) ; :: thesis:

end;

then reconsider KWJ = k . w1 as Nat by NUMBERS:19, W1, XXREAL_0:9;
KWJ <= 0 by NAT_1:13, W1;
hence x in { w where w is Element of Omega : k . w <= 0 } by W1; :: thesis:

end;

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:

end;

T1: 0 in StoppingSet T ;
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:

end;

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

end;

hence S₁[ 0 ] ; :: thesis:

end;

J11: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume S₁[n] ; :: thesis:
( (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

assume N01: (n + 1) + 1 in StoppingSet T ; :: thesis:
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

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

proof

let x be object ; :: thesis:
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:

proof

assume x in { w where w is Element of Omega : k . w < (n + 1) + 1 } ; :: thesis:
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

(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:

end;

consider w2 being Element of NAT such that
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:

end;

assume x in { w where w is Element of Omega : k . w <= n + 1 } ; :: thesis:
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

not k . w3 in {+infty}

proof

n + 1 < +infty by XXREAL_0:9, NUMBERS:19;
hence not k . w3 in {+infty} by TARSKI:def 1, QZ1; :: thesis:

end;

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

end;

then consider w2 being Element of NAT such that
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:

end;

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:

end;

s1: n + 1 in StoppingSet T

proof

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:

end;

( n + 1 in StoppingSet T & n + 1 <= (n + 1) + 1 ) by NAT_1:13, s1;
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:

end;

hence S₁[n + 1] ; :: thesis:

end;

Q1: for n being Nat holds S₁[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

proof

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

proof

per cases ;

suppose S1: t = 0 ; :: thesis:

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { w where w is Element of Omega : k . w < 0 } ; :: thesis:
then consider w being Element of Omega such that
TT: ( x = w & k . w < 0 ) ;
k . w >= 0

proof

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

per cases by TARSKI:def 1;

suppose k . w in StoppingSet T ; :: thesis:

then ex t being Element of NAT st
( t = k . w & 0 <= t & t <= T ) ;
hence k . w >= 0 ; :: thesis:

end;

suppose k . w = +infty ; :: thesis:

hence k . w >= 0 ; :: thesis:

end;

hence x in {} by TT; :: thesis:

end;

reconsider M = M as SigmaField of Omega ;
{} 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:

end;

suppose t > 0 ; :: thesis:

then { w where w is Element of Omega : k . w < (t - 1) + 1 } is Element of MyFunc . ((t - 1) + 1) by Q1;
hence { w where w is Element of Omega : k . w < t } is Element of M ; :: thesis:

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:

end;

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

proof

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

proof

let x be object ; :: thesis:
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:

proof

assume x in { w where w is Element of Omega : k . w <= t } \ { w where w is Element of Omega : k . w < t } ; :: thesis:
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

( k . w1 <= t & k . w1 >= t implies k . w1 = t )

proof

assume Q0: ( k . w1 <= t & k . w1 >= t ) ; :: thesis:
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:

end;

hence w1 in { w where w is Element of Omega : k . w = t } by JJJ1, JJJ; :: thesis:

end;

hence x in { w where w is Element of Omega : k . w = t } by JJJ1; :: thesis:

end;

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

end;

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:

end;

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

end;

hence k is_StoppingTime_wrt MyFunc,T ; :: thesis: