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
for k being Nat holds d tolerates Start-At (k,S)
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
for k being Nat holds d tolerates Start-At (k,S)
let d be data-only PartState of S; :: thesis: for k being Nat holds d tolerates Start-At (k,S)
let k be Nat; :: thesis: d tolerates Start-At (k,S)
dom d misses dom (Start-At (k,S)) by Th10, ZFMISC_1:50;
hence d tolerates Start-At (k,S) by PARTFUN1:56; :: thesis: verum