let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st s . (intloc 0) = 1 & IC s = 0 holds
s +* I = s +* (Initialized I)
let I be Program of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 & IC s = 0 implies s +* I = s +* (Initialized I) )
assume that
A1: s . (intloc 0) = 1 and
A2: IC s = 0 ; :: thesis: s +* I = s +* (Initialized I)
A3: IC SCM+FSA in dom s by COMPOS_1:9;
thus s +* (Initialized I) = s +* (Initialize I) by A1, SCMFSA8C:18
.= Initialize (s +* I) by FUNCT_4:15
.= (Initialize s) +* I by COMPOS_1:83
.= s +* I by A2, A3, FUNCT_7:111 ; :: thesis: verum