let M be non empty addLoopStr ; :: thesis: for p being FinSequence of the carrier of M
for k being Nat st k in dom p holds
Del (p,k,k) = Del (p,k)
let p be FinSequence of the carrier of M; :: thesis: for k being Nat st k in dom p holds
Del (p,k,k) = Del (p,k)
let k be Nat; :: thesis: ( k in dom p implies Del (p,k,k) = Del (p,k) )
assume A1: k in dom p ; :: thesis: Del (p,k,k) = Del (p,k)
then Seg (len p) <> {} by FINSEQ_1:def 3;
then A2: len p <> 0 ;
reconsider p0 = p as FinSequence of the carrier of M ;
reconsider m = (len p0) - 1 as Nat by A2;
A3: len p0 = m + 1 ;
A4: ( len p0 = m + 1 & k in dom p0 ) by A1;
A5: ( 1 <= k & k <= len p0 ) by A1, FINSEQ_3:25;
then A6: len (p0 | (k -' 1)) = k -' 1 by NAT_D:44, FINSEQ_1:59;
A7: len (p0 /^ k) = (len p0) - k by A5, RFINSEQ:def 1;
A8: len (Del (p,k,k)) = (len (p0 | (k -' 1))) + (len (p0 /^ k)) by FINSEQ_1:22
.= (k -' 1) + ((len p0) - k) by A6, A5, RFINSEQ:def 1
.= (k - 1) + ((len p0) - k) by A5, XREAL_1:233
.= (len p0) - 1 ;
A9: for i being Nat st i in dom (Del (p,k,k)) holds
(Del (p,k,k)) . i = (Del (p0,k)) . i

proof

let i be Nat; :: thesis: ( i in dom (Del (p,k,k)) implies (Del (p,k,k)) . i = (Del (p0,k)) . i )
assume A10: i in dom (Del (p,k,k)) ; :: thesis: (Del (p,k,k)) . i = (Del (p0,k)) . i
then i in Seg (len (Del (p0,k))) by A8, A4, FINSEQ_3:109, FINSEQ_1:def 3;
then A12: ( 1 <= i & i <= len (Del (p0,k)) ) by FINSEQ_1:1;

per cases ( i < k or k <= i ) ;

suppose A13: i < k ; :: thesis: (Del (p,k,k)) . i = (Del (p0,k)) . i

then A14: i <= k -' 1 by NAT_D:49;
1 <= i by A10, FINSEQ_3:25;
then i in Seg (len (p0 | (k -' 1))) by A14, A6;
then i in dom (p0 | (k -' 1)) by FINSEQ_1:def 3;
then (Del (p,k,k)) . i = (p0 | (k -' 1)) . i by FINSEQ_1:def 7
.= p0 . i by A14, FINSEQ_3:112 ;
hence (Del (p,k,k)) . i = (Del (p0,k)) . i by A13, FINSEQ_3:110; :: thesis: verum

end;

suppose A16: k <= i ; :: thesis: (Del (p,k,k)) . i = (Del (p0,k)) . i

then A17: ( k <= i & i <= m ) by A4, FINSEQ_3:109, A12;
A18: k -' 1 = k - 1 by A1, FINSEQ_3:25, XREAL_1:233;
k - 1 < k by XREAL_1:30;
then k -' 1 < i by A16, A18, XXREAL_0:2;
then len (p0 | (k -' 1)) < i by A5, NAT_D:44, FINSEQ_1:59;
then i - (len (p0 | (k -' 1))) > 0 by XREAL_1:50;
then i - (len (p0 | (k -' 1))) in NAT by INT_1:3;
then reconsider j = i - (len (p0 | (k -' 1))) as Nat ;
k <= m by A17, XXREAL_0:2;
then m - k >= 0 by XREAL_1:48;
then (m - k) + 1 > 0 ;
then (len p0) - k in NAT by INT_1:3;
then reconsider s = (len p0) - k as Nat ;
A23: dom (p0 /^ k) = Seg s by A7, FINSEQ_1:def 3;
A24: j = i - (k -' 1) by A5, NAT_D:44, FINSEQ_1:59;
then A25: i = j + (k -' 1) ;
A26: ((len p0) - k) - (i - (k -' 1)) = ((len p0) - i) - 1 by A18;
m - i >= 0 by A17, XREAL_1:48;
then A28: j <= s by A24, A26, XREAL_1:49;
A29: i - k >= k - k by A16, XREAL_1:6;
(i - (k -' 1)) - 1 = (i - (k - 1)) - 1 by A1, FINSEQ_3:25, XREAL_1:233
.= i - k ;
then ((i - (k -' 1)) - 1) + 1 >= 0 + 1 by A29, XREAL_1:6;
then 1 <= j by A5, NAT_D:44, FINSEQ_1:59;
then A32: j in Seg s by A28;
then A33: (Del (p,k,k)) . i = (p0 /^ k) . j by FINSEQ_1:def 7, A23, A25;
j in dom (p0 /^ k) by A32, A7, FINSEQ_1:def 3;
then A35: (p0 /^ k) . j = p0 . (k + j) by FINSEQ_5:27;
A36: j = i - (k -' 1) by A5, NAT_D:44, FINSEQ_1:59;
k -' 1 = k - 1 by A1, FINSEQ_3:25, XREAL_1:233;
then k + j = i + 1 by A36;
hence (Del (p,k,k)) . i = (Del (p0,k)) . i by A17, A1, A3, FINSEQ_3:111, A33, A35; :: thesis: verum

end;

end;

end;

dom (Del (p,k,k)) = Seg (len (Del (p0,k))) by A8, A4, FINSEQ_3:109, FINSEQ_1:def 3
.= dom (Del (p0,k)) by FINSEQ_1:def 3 ;
hence Del (p,k,k) = Del (p,k) by A9; :: thesis: verum