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 loc,val,size are_correct_wrt d1 holds
for n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
let V, A be set ; :: thesis: for val being Function
for loc being V -valued Function
for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
let val be Function; :: thesis: for loc being V -valued Function
for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
let loc be V -valued Function; :: thesis: for d1 being NonatomicND of V,A st loc,val,size are_correct_wrt d1 holds
for n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
let d1 be NonatomicND of V,A; :: thesis: ( loc,val,size are_correct_wrt d1 implies for n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) )
set F = LocalOverlapSeq (A,loc,val,d1,size);
assume that
A1: not V is empty and
A2: A is_without_nonatomicND_wrt V and
A3: val is_valid_wrt d1 and
A4: dom (LocalOverlapSeq (A,loc,val,d1,size)) c= dom val ; :: according to NOMIN_7:def 7 :: thesis: for n being Nat st 1 <= n & n <= size holds
dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
let n be Nat; :: thesis: ( 1 <= n & n <= size implies dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) )
assume that
A5: 1 <= n and
A6: n <= size ; :: thesis: dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n)
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= size implies dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . $1) );
A7: S₁[ 0 ] ;
A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A9: S₁[k] and
A10: 1 <= k + 1 and
A11: k + 1 <= size ; :: thesis: dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1))
A12: len (LocalOverlapSeq (A,loc,val,d1,size)) = size by Def4;

per cases ( k = 0 or k > 0 ) ;

suppose A13: k = 0 ; :: thesis: dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1))

set v = loc /. 1;
set D = denaming (V,A,(val . 1));
A14: dom (denaming (V,A,(val . 1))) = { d where d is NonatomicND of V,A : val . 1 in dom d } by NOMIN_1:def 18;
1 <= len (LocalOverlapSeq (A,loc,val,d1,size)) by A10, A11, A12, XXREAL_0:2;
then 1 in dom (LocalOverlapSeq (A,loc,val,d1,size)) by FINSEQ_3:25;
then val . 1 in rng val by A4, FUNCT_1:def 3;
then d1 in dom (denaming (V,A,(val . 1))) by A3, A14;
then reconsider d2 = (denaming (V,A,(val . 1))) . d1 as TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;
A15: (LocalOverlapSeq (A,loc,val,d1,size)) . 1 = local_overlapping (V,A,d1,d2,(loc /. 1)) by Def4;
dom (local_overlapping (V,A,d1,d2,(loc /. 1))) = {(loc /. 1)} \/ (dom d1) by A1, A2, NOMIN_4:4;
hence dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) by A13, A15, XBOOLE_1:7; :: thesis: verum

end;

suppose k > 0 ; :: thesis: dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1))

then A16: 0 + 1 <= k by NAT_1:13;
A17: k <= k + 1 by NAT_1:12;
then A18: dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . k) by A9, A11, A16, XXREAL_0:2;
k + 0 < k + 1 by XREAL_1:8;
then A19: k < size by A11, XXREAL_0:2;
k + 1 in dom (LocalOverlapSeq (A,loc,val,d1,size)) by A11, A12, FINSEQ_3:25, NAT_1:12;
then val . (k + 1) in rng val by A4, FUNCT_1:def 3;
then dom ((LocalOverlapSeq (A,loc,val,d1,size)) . k) c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) by A1, A2, A3, A16, A18, A19, Th6;
hence dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . (k + 1)) by A17, A9, A11, A16, XXREAL_0:2; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A8);
hence dom d1 c= dom ((LocalOverlapSeq (A,loc,val,d1,size)) . n) by A5, A6; :: thesis: verum