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
for i, j being Nat holds IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over 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 Th53
.= IncIC (p,(i + j)) by FUNCT_4:114 ; :: thesis: verum