let I be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st Initialized I c= s holds
IC s = 0
let s be State of SCM+FSA; :: thesis: ( Initialized I c= s implies IC s = 0 )
A1: ( IC (Initialized I) = 0 & IC SCM+FSA in dom (Initialized I) ) by SCMFSA6A:24, SCMFSA6A:25;
assume Initialized I c= s ; :: thesis: IC s = 0
hence IC s = 0 by A1, GRFUNC_1:8; :: thesis: verum