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 DecIC ((DecIC (p,i)),j) = DecIC (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 DecIC ((DecIC (p,i)),j) = DecIC (p,(i + j))
let p be PartState of S; :: thesis: for i, j being Nat holds DecIC ((DecIC (p,i)),j) = DecIC (p,(i + j))
let i, j be Nat; :: thesis: DecIC ((DecIC (p,i)),j) = DecIC (p,(i + j))
thus DecIC ((DecIC (p,i)),j) = (p +* (Start-At (((IC p) -' i),S))) +* (Start-At ((((IC p) -' i) -' j),S)) by Th65
.= (p +* (Start-At (((IC p) -' i),S))) +* (Start-At (((IC p) -' (i + j)),S)) by NAT_2:30
.= DecIC (p,(i + j)) by FUNCT_4:114 ; :: thesis: verum