let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds DataPart s = DataPart ((Initialize s) +* I)
let I be Program of SCMPDS ; :: thesis: DataPart s = DataPart ((Initialize s) +* I)
I1: (Initialize s) +* I = s +* (Initialize I) by SCMPDS_4:5;
thus DataPart s = DataPart ((Initialize s) +* I) by Th8, I1; :: thesis: verum