let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated Mem-Struct of 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 IC-Ins-separated Mem-Struct of 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 (Start-At (k,S)) = {(IC )} by FUNCOP_1:13;
then dom d misses dom (Start-At (k,S)) by Th57, ZFMISC_1:50;
hence d tolerates Start-At (k,S) by PARTFUN1:56; :: thesis: verum