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 = s +* (Initialize ((intloc 0) .--> 1))
let I be Program of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 & IC s = 0 implies s = s +* (Initialize ((intloc 0) .--> 1)) )
assume that
A1: s . (intloc 0) = 1 and
A2: IC s = 0 ; :: thesis: s = s +* (Initialize ((intloc 0) .--> 1))
A3: IC in dom s by COMPOS_1:9;
thus s +* (Initialize ((intloc 0) .--> 1)) = Initialize s by A1, SCMFSA8C:18
.= s by A2, A3, FUNCT_7:111 ; :: thesis: verum