let N be with_zero set ; 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 DecIC ((p +* d),k) = (DecIC (p,k)) +* d
let S be 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 DecIC ((p +* d),k) = (DecIC (p,k)) +* d
let p be PartState of S; for d being data-only PartState of S
for k being Nat holds DecIC ((p +* d),k) = (DecIC (p,k)) +* d
let d be data-only PartState of S; for k being Nat holds DecIC ((p +* d),k) = (DecIC (p,k)) +* d
let k be Nat; DecIC ((p +* d),k) = (DecIC (p,k)) +* d
A1:
d tolerates Start-At (((IC p) -' k),S)
by Th23;
thus DecIC ((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
.=
(DecIC (p,k)) +* d
by FUNCT_4:14
; verum