A0: dom k = Omega by FUNCT_2:def 1;

hereby :: 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 )

assume A1: 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
let t be Element of StoppingSet T; :: thesis: { w where w is Element of Omega : k . w = t } in MyFunc . t
{ w where w is Element of Omega : k . w = t } = Coim (k,t) by A0, L;
hence { w where w is Element of Omega : k . w = t } in MyFunc . t by A1; :: thesis: verum

end;

assume A2: 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
let t be Element of StoppingSet T; :: according to FINANCE4:def 4 :: thesis: Coim (k,t) in MyFunc . t
{ w where w is Element of Omega : k . w = t } = Coim (k,t) by A0, L;
hence Coim (k,t) in MyFunc . t by A2; :: thesis: verum