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