let s be State of ; :: thesis: for I being Program of holds DataPart s = DataPart (s +* (Initialized I))
let I be Program of ; :: thesis: DataPart s = DataPart (s +* (Initialized I))
Initialized I = I +* (Start-At (inspos 0 )) by SCMPDS_4:def 2;
hence DataPart s = DataPart (s +* (Initialized I)) by Th8; :: thesis: verum