dom (Start-At l,S) = {(IC S)} by FUNCOP_1:19;
hence IC S in dom (Start-At l,S) by TARSKI:def 1; :: according to COMPOS_1:def 16 :: thesis: IC (Start-At l,S) = l
thus IC (Start-At l,S) = l by FUNCOP_1:87; :: thesis: verum