let M be non empty addLoopStr ; :: thesis: for p being FinSequence of the carrier of M
for n, i being Nat st n in dom p & i in dom ((p | (n -' 1)) ^ (p /^ n)) holds
( ( i <= n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . i ) & ( i > n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . (i + 1) ) & i + 1 in dom p & len ((p | (n -' 1)) ^ (p /^ n)) = (len p) - 1 )
let p be FinSequence of the carrier of M; :: thesis: for n, i being Nat st n in dom p & i in dom ((p | (n -' 1)) ^ (p /^ n)) holds
( ( i <= n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . i ) & ( i > n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . (i + 1) ) & i + 1 in dom p & len ((p | (n -' 1)) ^ (p /^ n)) = (len p) - 1 )
let n, i be Nat; :: thesis: ( n in dom p & i in dom ((p | (n -' 1)) ^ (p /^ n)) implies ( ( i <= n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . i ) & ( i > n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . (i + 1) ) & i + 1 in dom p & len ((p | (n -' 1)) ^ (p /^ n)) = (len p) - 1 ) )
set a = p | (n -' 1);
set b = p /^ n;
set q = (p | (n -' 1)) ^ (p /^ n);
assume that
A1: n in dom p and
A2: i in dom ((p | (n -' 1)) ^ (p /^ n)) ; :: thesis: ( ( i <= n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . i ) & ( i > n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . (i + 1) ) & i + 1 in dom p & len ((p | (n -' 1)) ^ (p /^ n)) = (len p) - 1 )
dom p = Seg (len p) by FINSEQ_1:def 3;
then A4: ( 1 <= n & n <= len p ) by A1, FINSEQ_1:1;
A5: n <= len p by A1, FINSEQ_3:25;
then A6: len (p | (n -' 1)) = n -' 1 by FINSEQ_1:59, NAT_D:44;
A7: (len p) -' n = (len p) - n by A5, XREAL_1:233;
A8: len (p /^ n) = (len p) - n by A5, RFINSEQ:def 1
.= (len p) -' n by A5, XREAL_1:233 ;
then A9: dom (p /^ n) = Seg ((len p) -' n) by FINSEQ_1:def 3;
A10: len ((p | (n -' 1)) ^ (p /^ n)) = (len (p | (n -' 1))) + (len (p /^ n)) by FINSEQ_1:22
.= (n -' 1) + ((len p) - n) by A6, A8, A5, XREAL_1:233
.= (n - 1) + ((len p) - n) by A4, XREAL_1:233
.= (len p) - 1 ;
A11: dom ((p | (n -' 1)) ^ (p /^ n)) = Seg (len ((p | (n -' 1)) ^ (p /^ n))) by FINSEQ_1:def 3;
then ( 1 <= i & i <= (len p) - 1 ) by A10, A2, FINSEQ_1:1;
then A12: ( 1 + 1 <= i + 1 & i + 1 <= ((len p) - 1) + 1 ) by XREAL_1:6;
1 <= i + 1 by NAT_1:14;
then A13: i + 1 in Seg (len p) by A12;
then A14: i + 1 in dom p by FINSEQ_1:def 3;
A15: ( i <= n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . i )

proof

assume A16: i <= n -' 1 ; :: thesis: ((p | (n -' 1)) ^ (p /^ n)) . i = p . i
1 <= i by A2, FINSEQ_3:25;
then i in Seg (n -' 1) by A16;
then i in dom (p | (n -' 1)) by A6, FINSEQ_1:def 3;
then ((p | (n -' 1)) ^ (p /^ n)) . i = (p | (n -' 1)) . i by FINSEQ_1:def 7
.= p . i by A16, FINSEQ_3:112 ;
hence ((p | (n -' 1)) ^ (p /^ n)) . i = p . i ; :: thesis: verum

end;

( i > n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . (i + 1) )

proof

assume A18: i > n -' 1 ; :: thesis: ((p | (n -' 1)) ^ (p /^ n)) . i = p . (i + 1)
then reconsider j = i - (n -' 1) as Nat by NAT_1:21;
A19: i - (n -' 1) > (n -' 1) - (n -' 1) by A18, XREAL_1:14;
then A20: j >= 1 by NAT_1:14;
A21: i <= (len p) - 1 by A11, A10, A2, FINSEQ_1:1;
A22: (len (p | (n -' 1))) + 0 < (len (p | (n -' 1))) + j by A19, XREAL_1:8;
A23: i <= len ((p | (n -' 1)) ^ (p /^ n)) by A11, A2, FINSEQ_1:1;
A24: j + n = (i - (n - 1)) + n by A4, XREAL_1:233
.= i + 1 ;
((len p) - 1) - (n -' 1) = ((len p) - 1) - (n - 1) by A4, XREAL_1:233
.= (len p) - n ;
then j <= (len p) - n by A21, XREAL_1:6;
then A25: j in dom (p /^ n) by A20, A9, A7;
then (p /^ n) . j = (p /^ n) /. j by PARTFUN1:def 6
.= p /. (i + 1) by A24, FINSEQ_5:27, A25
.= p . (i + 1) by A14, PARTFUN1:def 6 ;
hence ((p | (n -' 1)) ^ (p /^ n)) . i = p . (i + 1) by FINSEQ_1:24, A6, A22, A23; :: thesis: verum

end;

hence ( ( i <= n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . i ) & ( i > n -' 1 implies ((p | (n -' 1)) ^ (p /^ n)) . i = p . (i + 1) ) & i + 1 in dom p & len ((p | (n -' 1)) ^ (p /^ n)) = (len p) - 1 ) by A15, A13, FINSEQ_1:def 3, A10; :: thesis: verum