A1: p | NAT = {} by Def29;
thus (DecIC (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 A1, Th27
.= {} ; :: according to COMPOS_1:def 29 :: thesis: verum