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 k being Nat st IC in dom p holds
DecIC ((IncIC (p,k)),k) = p
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for p being PartState of S
for k being Nat st IC in dom p holds
DecIC ((IncIC (p,k)),k) = p
let p be PartState of S; :: thesis: for k being Nat st IC in dom p holds
DecIC ((IncIC (p,k)),k) = p
let k be Nat; :: thesis: ( IC in dom p implies DecIC ((IncIC (p,k)),k) = p )
assume A1: IC in dom p ; :: thesis: DecIC ((IncIC (p,k)),k) = p
thus DecIC ((IncIC (p,k)),k) = (IncIC (p,k)) +* (Start-At ((((IC p) + k) -' k),S)) by Th53
.= (IncIC (p,k)) +* (Start-At ((IC p),S)) by NAT_D:34
.= p +* (Start-At ((IC p),S)) by Th36
.= p by A1, FUNCT_4:7, FUNCT_4:98 ; :: thesis: verum