A: p | NAT = {} by Def29;
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