let N be with_zero set ; :: thesis: for S being Mem-Struct over N
for p being data-only PartState of S holds DataPart p = p
let S be Mem-Struct over N; :: thesis: for p being data-only PartState of S holds DataPart p = p
let p be data-only PartState of S; :: thesis: DataPart p = p
dom p c= Data-Locations by Th6;
hence DataPart p = p by RELAT_1:68; :: thesis: verum