let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st IC in dom p holds
dom p = {(IC )} \/ (dom (DataPart p))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for p being PartState of S st IC in dom p holds
dom p = {(IC )} \/ (dom (DataPart p))
let p be PartState of S; :: thesis: ( IC in dom p implies dom p = {(IC )} \/ (dom (DataPart p)) )
assume IC in dom p ; :: thesis: dom p = {(IC )} \/ (dom (DataPart p))
then A1: p = (Start-At ((IC p),S)) +* (DataPart p) by Th19;
dom p = (dom (Start-At ((IC p),S))) \/ (dom (DataPart p)) by A1, FUNCT_4:def 1
.= {(IC )} \/ (dom (DataPart p)) ;
hence dom p = {(IC )} \/ (dom (DataPart p)) ; :: thesis: verum