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
for i, j being Nat holds IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S
for i, j being Nat holds IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))
let p be PartState of S; :: thesis: for i, j being Nat holds IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))
let i, j be Nat; :: thesis: IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))
thus IncIC ((IncIC (p,i)),j) = (p +* (Start-At (((IC p) + i),S))) +* (Start-At ((((IC p) + i) + j),S)) by Th54
.= IncIC (p,(i + j)) by FUNCT_4:122 ; :: thesis: verum