let size be non zero Nat; :: thesis: for V, A being set
for val being Function
for loc being b₁ -valued Function
for d1 being NonatomicND of V,A st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1))
let V, A be set ; :: thesis: for val being Function
for loc being V -valued Function
for d1 being NonatomicND of V,A st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1))
let val be Function; :: thesis: for loc being V -valued Function
for d1 being NonatomicND of V,A st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1))
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A st not V is empty & A is_without_nonatomicND_wrt V holds
for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1))
let d1 be NonatomicND of V,A; :: thesis: ( not V is empty & A is_without_nonatomicND_wrt V implies for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) )
set F = LocalOverlapSeq (A,loc,val,d1,size);
assume A1: ( not V is empty & A is_without_nonatomicND_wrt V ) ; :: thesis: for n being Nat st 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) holds
dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1))
let n be Nat; :: thesis: ( 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) implies dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) )
assume ( 1 <= n & n < size & val . (n + 1) in dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) ) ; :: thesis: dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1))
then dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) = {(loc /. (n + 1))} \/ (dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)) by A1, Th5;
hence dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (n + 1)) by XBOOLE_1:7; :: thesis: verum