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 d being data-only PartState of S
for k being Nat holds IncIC ((p +* d),k) = (IncIC (p,k)) +* d
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for p being PartState of S
for d being data-only PartState of S
for k being Nat holds IncIC ((p +* d),k) = (IncIC (p,k)) +* d
let p be PartState of S; :: thesis: for d being data-only PartState of S
for k being Nat holds IncIC ((p +* d),k) = (IncIC (p,k)) +* d
let d be data-only PartState of S; :: thesis: for k being Nat holds IncIC ((p +* d),k) = (IncIC (p,k)) +* d
let k be Nat; :: thesis: IncIC ((p +* d),k) = (IncIC (p,k)) +* d
A1: d tolerates Start-At (((IC p) + k),S) by Th23;
thus IncIC ((p +* d),k) = (p +* d) +* (Start-At (((IC p) + k),S)) by Th11
.= p +* (d +* (Start-At (((IC p) + k),S))) by FUNCT_4:14
.= p +* ((Start-At (((IC p) + k),S)) +* d) by A1, FUNCT_4:34
.= (IncIC (p,k)) +* d by FUNCT_4:14 ; :: thesis: verum