let s be State of SCM+FSA; :: thesis: Initialized (Initialized s) = Initialized s
A1: IC (Initialized s) = 0 by SCMFSA6C:3;
(Initialized s) . (intloc 0) = 1 by SCMFSA6C:3;
hence Initialized (Initialized s) = Initialized s by A1, Th14; :: thesis: verum