let a be Int_position ; :: thesis: for s being State of SCMPDS
for I being Program of SCMPDS holds ((Initialize s) +* I) . a = s . a
let s be State of SCMPDS; :: thesis: for I being Program of SCMPDS holds ((Initialize s) +* I) . a = s . a
let I be Program of SCMPDS; :: thesis: ((Initialize s) +* I) . a = s . a
I1: s +* (Initialize I) = (Initialize s) +* I by COMPOS_1:125;
not a in dom (Initialize I) by SCMPDS_4:31;
hence ((Initialize s) +* I) . a = s . a by I1, FUNCT_4:12; :: thesis: verum