let k be Nat; :: thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for d being data-only PartState of S holds d +* (Start-At (k,S)) = (Start-At (k,S)) +* d
let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for d being data-only PartState of S holds d +* (Start-At (k,S)) = (Start-At (k,S)) +* d
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for d being data-only PartState of S holds d +* (Start-At (k,S)) = (Start-At (k,S)) +* d
let d be data-only PartState of S; :: thesis: d +* (Start-At (k,S)) = (Start-At (k,S)) +* d
d tolerates Start-At (k,S) by Th23;
hence d +* (Start-At (k,S)) = (Start-At (k,S)) +* d by FUNCT_4:34; :: thesis: verum