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