let s be State of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies IC s = 0 )
assume Initialize ((intloc 0) .--> 1) c= s ; :: thesis: IC s = 0
hence IC s = 0 by COMPOS_1:143; :: thesis: verum