let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS st Initialize I c= s holds
IC s = 0
let I be Program of SCMPDS ; :: thesis: ( Initialize I c= s implies IC s = 0 )
A1: IC (Initialize I) = 0 by COMPOS_1:def 16;
A2: IC SCMPDS in dom (Initialize I) by COMPOS_1:def 16;
assume Initialize I c= s ; :: thesis: IC s = 0
hence IC s = 0 by A1, A2, GRFUNC_1:8; :: thesis: verum