let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for T being non zero Nat
for MyFunc being Filtration of StoppingSet T,Sigma holds
not for k1, k2 being StoppingTime_Func of MyFunc holds k1 + k2 is StoppingTime_Func of MyFunc
let Sigma be SigmaField of Omega; :: thesis: for T being non zero Nat
for MyFunc being Filtration of StoppingSet T,Sigma holds
not for k1, k2 being StoppingTime_Func of MyFunc holds k1 + k2 is StoppingTime_Func of MyFunc
let T be non zero Nat; :: thesis: for MyFunc being Filtration of StoppingSet T,Sigma holds
not for k1, k2 being StoppingTime_Func of MyFunc holds k1 + k2 is StoppingTime_Func of MyFunc
let MyFunc be Filtration of StoppingSet T,Sigma; :: thesis: not for k1, k2 being StoppingTime_Func of MyFunc holds k1 + k2 is StoppingTime_Func of MyFunc
T in NAT by ORDINAL1:def 12;
then ( T in StoppingSet T or T in {+infty} ) ;
then reconsider MyT = T as Element of StoppingSetExt T by XBOOLE_0:def 3;
consider k1 being Function of Omega,(StoppingSetExt T) such that
A1: ( k1 = Omega --> MyT & k1 is_StoppingTime_wrt MyFunc,T ) by FINANCE4:3;
reconsider k1 = k1 as StoppingTime_Func of MyFunc by A1, Def1;
consider k2 being Function of Omega,(StoppingSetExt T) such that
A2: ( k2 = Omega --> MyT & k2 is_StoppingTime_wrt MyFunc,T ) by FINANCE4:3;
reconsider k2 = k2 as StoppingTime_Func of MyFunc by A2, Def1;
take k1 ; :: thesis: not for k2 being StoppingTime_Func of MyFunc holds k1 + k2 is StoppingTime_Func of MyFunc
take k2 ; :: thesis: k1 + k2 is not StoppingTime_Func of MyFunc
F1: not T + T in {+infty} by TARSKI:def 1;
ex w being Element of dom (k1 + k2) st
( w in dom (k1 + k2) & not (k1 + k2) . w in StoppingSetExt T )

proof

consider w2 being object such that
C1: w2 in dom (k1 + k2) by XBOOLE_0:def 1;
reconsider w2 = w2 as Element of Omega by C1;
e3: ( k1 . w2 = T & k2 . w2 = T ) by A1, FUNCOP_1:7, A2;
XX: T + T = (k1 . w2) + (k2 . w2) by e3, XXREAL_3:def 2
.= (k1 + k2) . w2 by C1, Def888 ;
not (k1 + k2) . w2 in StoppingSetExt T

proof

not T + T in StoppingSetExt T

proof

not T + T in { t where t is Element of NAT : ( 0 <= t & t <= T ) }

proof

for t2 being Element of NAT holds
( not t2 = T + T or not 0 <= t2 or not t2 <= T ) by NAT_1:16;
hence not T + T in { t where t is Element of NAT : ( 0 <= t & t <= T ) } ; :: thesis: verum

end;

hence not T + T in StoppingSetExt T by F1, XBOOLE_0:def 3; :: thesis: verum

end;

hence not (k1 + k2) . w2 in StoppingSetExt T by XX; :: thesis: verum

end;

hence ex w being Element of dom (k1 + k2) st
( w in dom (k1 + k2) & not (k1 + k2) . w in StoppingSetExt T ) by C1; :: thesis: verum

end;

hence k1 + k2 is not StoppingTime_Func of MyFunc by FUNCT_2:5; :: thesis: verum