let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of N
for p being PartState of S st IC in dom p holds
p = (DataPart p) +* (Start-At ((IC p),S))
let S be non empty IC-Ins-separated Mem-Struct of N; :: thesis: for p being PartState of S st IC in dom p holds
p = (DataPart p) +* (Start-At ((IC p),S))
let p be PartState of S; :: thesis: ( IC in dom p implies p = (DataPart p) +* (Start-At ((IC p),S)) )
B2: dom (Start-At ((IC p),S)) = {(IC )} by FUNCOP_1:13;
then A2: dom (DataPart p) misses dom (Start-At ((IC p),S)) by Th11, ZFMISC_1:50;
A5: dom (Start-At ((IC p),S)) misses dom (DataPart p) by B2, Th11, ZFMISC_1:50;
assume IC in dom p ; :: thesis: p = (DataPart p) +* (Start-At ((IC p),S))
then p = (Start-At ((IC p),S)) +* (DataPart p) by Th18;
then A7: p = (Start-At ((IC p),S)) \/ (DataPart p) by A5, FUNCT_4:31;
thus p = (DataPart p) +* (Start-At ((IC p),S)) by A2, A7, FUNCT_4:31; :: thesis: verum