let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of 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 IC-Ins-separated Mem-Struct of 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 Z: 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 Th54
.= (IncIC (p,k)) +* (Start-At ((IC p),S)) by NAT_D:34
.= p +* (Start-At ((IC p),S)) by Th199
.= p by Z, FUNCT_4:7, FUNCT_4:98 ; :: thesis: verum