let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being NAT -defined PartState of holds DataPart I = 0
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for I being NAT -defined PartState of holds DataPart I = 0
let I be NAT -defined PartState of ; :: thesis: DataPart I = 0
dom I c= NAT by RELAT_1:def 18;
then A1: dom I misses Data-Locations S by Th51, XBOOLE_1:63;
thus DataPart I = I | (Data-Locations S)
.= {} by A1, RELAT_1:95 ; :: thesis: verum