let q be PartState of S; :: thesis: ( q = p +* I implies q is k -started )
F: IC S in dom p by Def41;
assume Z: q = p +* I ; :: thesis: q is k -started
then dom q = (dom p) \/ (dom I) by FUNCT_4:def 1;
hence IC S in dom q by F, 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 S in dom I by Def21;
hence IC q = IC p by Z, FUNCT_4:12
.= k by Def41 ;
:: thesis: verum