A: p | NAT = {} by Defx;
thus (IncrIC p,k) | NAT = (p +* (Start-At ((IC p) + k),S)) | NAT
.= (p | NAT ) +* (ProgramPart (Start-At ((IC p) + k),S)) by FUNCT_4:75
.= {} +* {} by A, Th135
.= {} ; :: according to COMPOS_1:def 29 :: thesis: verum