let R be Ring; :: thesis: the carrier of (SCM R) \ {NAT} = SCM-Data-Loc
A1: not NAT in SCM-Data-Loc by AMI_2:20;
thus the carrier of (SCM R) \ {NAT} = SCM-Memory \ {NAT} by Def1
.= ({NAT} \/ SCM-Data-Loc) \ {NAT}
.= SCM-Data-Loc by A1, ZFMISC_1:117 ; :: thesis: verum