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
p = (Start-At ((IC p),S)) +* (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
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;
A2: {(IC )} \/ ( the carrier of S \ {(IC )}) = the carrier of S \/ {(IC )} by XBOOLE_1:39
.= the carrier of S by XBOOLE_1:12 ;
A3: dom p c= the carrier of S by RELAT_1:def 18;

A4: now :: thesis: for x being object st x in dom p holds
p . x = ((Start-At ((IC p),S)) +* (DataPart p)) . x

let x be object ; :: thesis: ( x in dom p implies p . b₁ = ((Start-At ((IC p),S)) +* (DataPart p)) . b₁ )
assume A5: 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 A5, A3, A2, XBOOLE_0:def 3;

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

IC in dom (Start-At ((IC p),S)) by TARSKI:def 1;
then A7: IC in (dom (Start-At ((IC p),S))) \/ (dom (DataPart p)) by XBOOLE_0:def 3;
A8: x = IC by A6, TARSKI:def 1;
not IC in dom (DataPart p) by Th3;
then ((Start-At ((IC p),S)) +* (DataPart p)) . x = (Start-At ((IC p),S)) . x by A8, A7, FUNCT_4:def 1
.= IC p by A8, FUNCOP_1:72 ;
hence p . x = ((Start-At ((IC p),S)) +* (DataPart p)) . x by A6, 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 A5, XBOOLE_0:def 4;
then A9: 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 A9, FUNCT_4:13
.= p . x by A9, FUNCT_1:47 ;
hence p . x = ((Start-At ((IC p),S)) +* (DataPart p)) . x ; :: thesis: verum

end;

end;

end;

A10: 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))
.= ((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 A2, XBOOLE_1:23
.= dom p by A10, XBOOLE_1:28 ;
hence p = (Start-At ((IC p),S)) +* (DataPart p) by A4; :: thesis: verum