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