let N be with_non-empty_elements set ; :: thesis: for S being Mem-Struct of N
for p being data-only PartState of S holds DataPart p = p
let S be Mem-Struct of 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 Th31;
hence DataPart p = p by RELAT_1:68; :: thesis: verum