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

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

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 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,Tassume 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;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

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