let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for p being FinPartState of S st IC S in dom p holds
p = ((Start-At (IC p)) +* (ProgramPart p)) +* (DataPart p)
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for p being FinPartState of S st IC S in dom p holds
p = ((Start-At (IC p)) +* (ProgramPart p)) +* (DataPart p)
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N; :: thesis: for p being FinPartState of S st IC S in dom p holds
p = ((Start-At (IC p)) +* (ProgramPart p)) +* (DataPart p)
let p be FinPartState of S; :: thesis: ( IC S in dom p implies p = ((Start-At (IC p)) +* (ProgramPart p)) +* (DataPart p) )
assume A1: IC S in dom p ; :: thesis: p = ((Start-At (IC p)) +* (ProgramPart p)) +* (DataPart p)
then A2: {(IC S)} is Subset of (dom p) by SUBSET_1:63;
A3: dom p c= the carrier of S by Th80;
A4: IL c= the carrier of S by Def3;
A5: ({(IC S)} \/ IL) \/ (the carrier of S \ ({(IC S)} \/ IL)) = the carrier of S \/ ({(IC S)} \/ IL) by XBOOLE_1:39
.= the carrier of S by A4, XBOOLE_1:8, XBOOLE_1:12 ;
A6: dom (((Start-At (IC p)) +* (ProgramPart p)) +* (DataPart p)) = (dom ((Start-At (IC p)) +* (ProgramPart p))) \/ (dom (DataPart p)) by FUNCT_4:def 1
.= ((dom (Start-At (IC p))) \/ (dom (ProgramPart p))) \/ (dom (DataPart p)) by FUNCT_4:def 1
.= ({(IC S)} \/ (dom (p | IL))) \/ (dom (DataPart p)) by FUNCOP_1:19
.= (((dom p) /\ {(IC S)}) \/ (dom (p | IL))) \/ (dom (p | (the carrier of S \ ({(IC S)} \/ IL)))) by A2, XBOOLE_1:28
.= (((dom p) /\ {(IC S)}) \/ ((dom p) /\ IL)) \/ (dom (p | (the carrier of S \ ({(IC S)} \/ IL)))) by RELAT_1:90
.= (((dom p) /\ {(IC S)}) \/ ((dom p) /\ IL)) \/ ((dom p) /\ (the carrier of S \ ({(IC S)} \/ IL))) by RELAT_1:90
.= ((dom p) /\ ({(IC S)} \/ IL)) \/ ((dom p) /\ (the carrier of S \ ({(IC S)} \/ IL))) by XBOOLE_1:23
.= (dom p) /\ the carrier of S by A5, XBOOLE_1:23
.= dom p by Th80, XBOOLE_1:28 ;

now

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

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

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

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

end;

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

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

end;

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

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

end;

end;

end;

hence p = ((Start-At (IC p)) +* (ProgramPart p)) +* (DataPart p) by A6, FUNCT_1:9; :: thesis: verum