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 p being PartState of S st IC in dom p holds
p = ((Start-At ((IC p),S)) +* (ProgramPart p)) +* (DataPart p)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S st IC in dom p holds
p = ((Start-At ((IC p),S)) +* (ProgramPart p)) +* (DataPart p)
let p be PartState of S; :: thesis: ( IC in dom p implies p = ((Start-At ((IC p),S)) +* (ProgramPart p)) +* (DataPart p) )
assume IC in dom p ; :: thesis: p = ((Start-At ((IC p),S)) +* (ProgramPart p)) +* (DataPart p)
then A1: {(IC )} is Subset of (dom p) by SUBSET_1:63;
A2: NAT c= the carrier of S by Def2;
A3: ({(IC )} \/ NAT) \/ ( the carrier of S \ ({(IC )} \/ NAT)) = the carrier of S \/ ({(IC )} \/ NAT) by XBOOLE_1:39
.= the carrier of S by A2, XBOOLE_1:8, 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)) +* (ProgramPart p)) +* (DataPart p)) . b₁ )
assume A6: x in dom p ; :: thesis: p . b₁ = (((Start-At ((IC p),S)) +* (ProgramPart p)) +* (DataPart p)) . b₁
then A7: ( x in {(IC )} \/ NAT or x in the carrier of S \ ({(IC )} \/ NAT) ) by A4, A3, XBOOLE_0:def 3;

per cases ( x in {(IC )} or x in the carrier of S \ ({(IC )} \/ NAT) or x in NAT ) by A7, XBOOLE_0:def 3;

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

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

end;

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

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

end;

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

then x in (dom p) /\ NAT by A6, XBOOLE_0:def 4;
then A14: x in dom (p | NAT) by RELAT_1:90;
dom (DataPart p) misses dom (ProgramPart p) by Th15;
then A15: not x in dom (DataPart p) by A14, XBOOLE_0:3;
A16: x in (dom (Start-At ((IC p),S))) \/ (dom (ProgramPart p)) by A14, XBOOLE_0:def 3;
then x in dom ((Start-At ((IC p),S)) +* (ProgramPart p)) by FUNCT_4:def 1;
then x in (dom ((Start-At ((IC p),S)) +* (ProgramPart p))) \/ (dom (DataPart p)) by XBOOLE_0:def 3;
then (((Start-At ((IC p),S)) +* (ProgramPart p)) +* (DataPart p)) . x = ((Start-At ((IC p),S)) +* (ProgramPart p)) . x by A15, FUNCT_4:def 1
.= (p | NAT) . x by A14, A16, FUNCT_4:def 1
.= p . x by A14, FUNCT_1:70 ;
hence p . x = (((Start-At ((IC p),S)) +* (ProgramPart p)) +* (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)) +* (ProgramPart p)) +* (DataPart p)) = (dom ((Start-At ((IC p),S)) +* (ProgramPart p))) \/ (dom (DataPart p)) by FUNCT_4:def 1
.= ((dom (Start-At ((IC p),S))) \/ (dom (ProgramPart p))) \/ (dom (DataPart p)) by FUNCT_4:def 1
.= ({(IC )} \/ (dom (p | NAT))) \/ (dom (DataPart p)) by FUNCOP_1:19
.= (((dom p) /\ {(IC )}) \/ (dom (p | NAT))) \/ (dom (p | ( the carrier of S \ ({(IC )} \/ NAT)))) by A1, XBOOLE_1:28
.= (((dom p) /\ {(IC )}) \/ ((dom p) /\ NAT)) \/ (dom (p | ( the carrier of S \ ({(IC )} \/ NAT)))) by RELAT_1:90
.= (((dom p) /\ {(IC )}) \/ ((dom p) /\ NAT)) \/ ((dom p) /\ ( the carrier of S \ ({(IC )} \/ NAT))) by RELAT_1:90
.= ((dom p) /\ ({(IC )} \/ NAT)) \/ ((dom p) /\ ( the carrier of S \ ({(IC )} \/ NAT))) by XBOOLE_1:23
.= (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)) +* (ProgramPart p)) +* (DataPart p) by A5, FUNCT_1:9; :: thesis: verum