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 COMPOS_1:125;
thus DataPart s = DataPart ((Initialize s) +* I) by Th8, I1; :: thesis: verum