Data-Locations = the carrier of (STC N) \ {0} by Def7
.= {0} \ {0} by Def7
.= {} by XBOOLE_1:37 ;
hence DataPart p is empty ; :: thesis: verum