let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds IC ((Initialize s) +* I) = 0
let I be Program of SCMPDS ; :: thesis: IC ((Initialize s) +* I) = 0
I1: s +* (Initialize I) = (Initialize s) +* I by SCMPDS_4:5;
thus IC ((Initialize s) +* I) = 0 by I1, FUNCT_4:26, SCMPDS_5:18; :: thesis: verum