let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for p being FinPartState of S st IC S 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 AMI-Struct of N; :: thesis: for p being FinPartState of S st IC S in dom p holds
p = ((Start-At (IC p),S) +* (ProgramPart p)) +* (DataPart p)
let p be FinPartState of S; :: thesis: ( IC S in dom p implies p = ((Start-At (IC p),S) +* (ProgramPart p)) +* (DataPart p) )
assume IC S in dom p ; :: thesis: p = ((Start-At (IC p),S) +* (ProgramPart p)) +* (DataPart p)
then A2: {(IC S)} is Subset of (dom p) by SUBSET_1:63;
A3: NAT c= the carrier of S by Def3;
A4: ({(IC S)} \/ NAT ) \/ (the carrier of S \ ({(IC S)} \/ NAT )) = the carrier of S \/ ({(IC S)} \/ NAT ) by XBOOLE_1:39
.= the carrier of S by A3, XBOOLE_1:8, XBOOLE_1:12 ;
A5: dom p c= the carrier of S by RELAT_1:def 18;

A6: now

let x be set ; :: thesis: ( x in dom p implies p . b₁ = (((Start-At (IC p),S) +* (ProgramPart p)) +* (DataPart p)) . b₁ )
assume A7: x in dom p ; :: thesis: p . b₁ = (((Start-At (IC p),S) +* (ProgramPart p)) +* (DataPart p)) . b₁
then A8: ( x in {(IC S)} \/ NAT or x in the carrier of S \ ({(IC S)} \/ NAT ) ) by A5, A4, XBOOLE_0:def 3;

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

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

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

end;

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

then x in (dom p) /\ (the carrier of S \ ({(IC S)} \/ NAT )) by A7, XBOOLE_0:def 4;
then A14: x in dom (p | (the carrier of S \ ({(IC S)} \/ NAT ))) by RELAT_1:90;
then x in (dom ((Start-At (IC p),S) +* (ProgramPart p))) \/ (dom (p | (the carrier of S \ ({(IC S)} \/ NAT )))) by XBOOLE_0:def 3;
then (((Start-At (IC p),S) +* (ProgramPart p)) +* (DataPart p)) . x = (p | (the carrier of S \ ({(IC S)} \/ NAT ))) . x by A14, 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;

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

then x in (dom p) /\ NAT by A7, XBOOLE_0:def 4;
then A15: x in dom (p | NAT ) by RELAT_1:90;
dom (DataPart p) misses dom (ProgramPart p) by Th104;
then A16: not x in dom (DataPart p) by A15, XBOOLE_0:3;
A17: x in (dom (Start-At (IC p),S)) \/ (dom (ProgramPart p)) by A15, 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 A16, FUNCT_4:def 1
.= (p | NAT ) . x by A15, A17, FUNCT_4:def 1
.= p . x by A15, FUNCT_1:70 ;
hence p . x = (((Start-At (IC p),S) +* (ProgramPart p)) +* (DataPart p)) . x ; :: thesis: verum

end;

end;

end;

X: 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 S)} \/ (dom (p | NAT ))) \/ (dom (DataPart p)) by FUNCOP_1:19
.= (((dom p) /\ {(IC S)}) \/ (dom (p | NAT ))) \/ (dom (p | (the carrier of S \ ({(IC S)} \/ NAT )))) by A2, XBOOLE_1:28
.= (((dom p) /\ {(IC S)}) \/ ((dom p) /\ NAT )) \/ (dom (p | (the carrier of S \ ({(IC S)} \/ NAT )))) by RELAT_1:90
.= (((dom p) /\ {(IC S)}) \/ ((dom p) /\ NAT )) \/ ((dom p) /\ (the carrier of S \ ({(IC S)} \/ NAT ))) by RELAT_1:90
.= ((dom p) /\ ({(IC S)} \/ NAT )) \/ ((dom p) /\ (the carrier of S \ ({(IC S)} \/ NAT ))) by XBOOLE_1:23
.= (dom p) /\ the carrier of S by A4, XBOOLE_1:23
.= dom p by X, XBOOLE_1:28 ;
hence p = ((Start-At (IC p),S) +* (ProgramPart p)) +* (DataPart p) by A6, FUNCT_1:9; :: thesis: verum