let q be PartState of S; :: thesis: ( q = p +* I implies q is k -started )
A1: IC in dom p by Def16;
assume A2: q = p +* I ; :: thesis: q is k -started
then dom q = (dom p) \/ (dom I) by FUNCT_4:def 1;
hence IC in dom q by A1, XBOOLE_0:def 3; :: according to COMPOS_1:def 16 :: thesis: IC q = k
dom I c= NAT by RELAT_1:def 18;
then not IC in dom I by Def12;
hence IC q = IC p by A2, FUNCT_4:12
.= k by Def16 ;
:: thesis: verum