A1: dom s = the carrier of SCM+FSA by PARTFUN1:def 4;
thus dom (Initialized s) = ((dom s) \/ {(intloc 0)}) \/ {(IC )} by SCMFSA6A:43
.= (dom s) \/ {(IC )} by A1, ZFMISC_1:46
.= dom s by COMPOS_1:9, ZFMISC_1:46
.= the carrier of SCM+FSA by PARTFUN1:def 4 ; :: according to PARTFUN1:def 4 :: thesis: verum