let p, q be PartState of SCM+FSA; :: thesis: IC in dom (p +* (Initialized q))
A: dom (p +* (Initialized q)) = (dom p) \/ (dom (Initialized q)) by FUNCT_4:def 1;
IC in dom (Initialized q) by Th24;
hence IC in dom (p +* (Initialized q)) by A, XBOOLE_0:def 3; :: thesis: verum