let n be Element of NAT ; :: thesis: for s being State of SCMPDS holds (Comput (ProgramPart s),s,n) | NAT = s | NAT
let s be State of SCMPDS ; :: thesis: (Comput (ProgramPart s),s,n) | NAT = s | NAT
for x being Element of NAT holds (Comput (ProgramPart s),s,n) . x = s . x by AMI_1:54;
hence (Comput (ProgramPart s),s,n) | NAT = s | NAT by SCMPDS_4:21; :: thesis: verum