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 = (Start-At ((IC p),S)) +* (DataPart p)
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 = (Start-At ((IC p),S)) +* (DataPart p)
let p be PartState of S; :: thesis: ( IC in dom p implies p = (Start-At ((IC p),S)) +* (DataPart p) )
assume IC in dom p ; :: thesis: p = (Start-At ((IC p),S)) +* (DataPart p)
then A1: {(IC )} is Subset of (dom p) by SUBSET_1:41;
A3: {(IC )} \/ ( the carrier of S \ {(IC )}) = the carrier of S \/ {(IC )} by XBOOLE_1:39
.= the carrier of S by XBOOLE_1:12 ;
A4: dom p c= the carrier of S by RELAT_1:def 18;

A5: now

let x be set ; :: thesis: ( x in dom p implies p . b₁ = ((Start-At ((IC p),S)) +* (DataPart p)) . b₁ )
assume A6: x in dom p ; :: thesis: p . b₁ = ((Start-At ((IC p),S)) +* (DataPart p)) . b₁

per cases ( x in {(IC )} or x in the carrier of S \ {(IC )} ) by A6, A4, A3, XBOOLE_0:def 3;

suppose A8: x in {(IC )} ; :: thesis: p . b₁ = ((Start-At ((IC p),S)) +* (DataPart p)) . b₁

{(IC )} = dom (Start-At ((IC p),S)) by FUNCOP_1:13;
then IC in dom (Start-At ((IC p),S)) by TARSKI:def 1;
then A10: IC in (dom (Start-At ((IC p),S))) \/ (dom (DataPart p)) by XBOOLE_0:def 3;
A12: x = IC by A8, TARSKI:def 1;
not IC in dom (DataPart p) by Th11;
then ((Start-At ((IC p),S)) +* (DataPart p)) . x = (Start-At ((IC p),S)) . x by A12, A10, FUNCT_4:def 1
.= IC p by A12, FUNCOP_1:72 ;
hence p . x = ((Start-At ((IC p),S)) +* (DataPart p)) . x by A8, TARSKI:def 1; :: thesis: verum

end;

suppose x in the carrier of S \ {(IC )} ; :: thesis: p . b₁ = ((Start-At ((IC p),S)) +* (DataPart p)) . b₁

then x in (dom p) /\ ( the carrier of S \ {(IC )}) by A6, XBOOLE_0:def 4;
then A13: x in dom (p | ( the carrier of S \ {(IC )})) by RELAT_1:61;
((Start-At ((IC p),S)) +* (DataPart p)) . x = (DataPart p) . x by A13, FUNCT_4:13
.= p . x by A13, FUNCT_1:47 ;
hence p . x = ((Start-At ((IC p),S)) +* (DataPart p)) . x ; :: thesis: verum

end;

end;

end;

A17: dom p c= the carrier of S by RELAT_1:def 18;
dom ((Start-At ((IC p),S)) +* (DataPart p)) = (dom (Start-At ((IC p),S))) \/ (dom (DataPart p)) by FUNCT_4:def 1
.= {(IC )} \/ (dom (DataPart p)) by FUNCOP_1:13
.= ((dom p) /\ {(IC )}) \/ (dom (p | ( the carrier of S \ {(IC )}))) by A1, XBOOLE_1:28
.= ((dom p) /\ {(IC )}) \/ ((dom p) /\ ( the carrier of S \ {(IC )})) by RELAT_1:61
.= (dom p) /\ the carrier of S by A3, XBOOLE_1:23
.= dom p by A17, XBOOLE_1:28 ;
hence p = (Start-At ((IC p),S)) +* (DataPart p) by A5, FUNCT_1:2; :: thesis: verum