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 COMPOS_1:125;
thus IC ((Initialize s) +* I) = 0 by I1, FUNCT_4:26, SCMPDS_5:18; :: thesis: verum