let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA holds I c= s +* (Initialized I)
let s be State of SCM+FSA ; :: thesis: I c= s +* (Initialized I)
( Initialized I c= s +* (Initialized I) & I c= Initialized I ) by FUNCT_4:26, SCMFSA6A:26;
hence I c= s +* (Initialized I) by XBOOLE_1:1; :: thesis: verum