let i, j be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st j + 1 = i & i in dom f holds
<*(f /. i)*> ^ (f /^ i) = f /^ j
let D be non empty set ; :: thesis: for f being FinSequence of D st j + 1 = i & i in dom f holds
<*(f /. i)*> ^ (f /^ i) = f /^ j
let f be FinSequence of D; :: thesis: ( j + 1 = i & i in dom f implies <*(f /. i)*> ^ (f /^ i) = f /^ j )
assume that
A1: j + 1 = i and
A2: i in dom f ; :: thesis: <*(f /. i)*> ^ (f /^ i) = f /^ j
set g = <*(f /. i)*> ^ (f /^ i);
A3: i <= len f by A2, FINSEQ_3:25;
j <= i by A1, NAT_1:11;
then A4: j <= len f by A3, XXREAL_0:2;
A5: len (<*(f /. i)*> ^ (f /^ i)) = (len (f /^ i)) + 1 by Th8;
then A6: len (<*(f /. i)*> ^ (f /^ i)) = ((len f) - i) + 1 by A3, RFINSEQ:def 1
.= (len f) - j by A1
.= len (f /^ j) by A4, RFINSEQ:def 1 ;

now :: thesis: for k being Nat st 1 <= k & k <= len (<*(f /. i)*> ^ (f /^ i)) holds
(<*(f /. i)*> ^ (f /^ i)) . k = (f /^ j) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (<*(f /. i)*> ^ (f /^ i)) implies (<*(f /. i)*> ^ (f /^ i)) . b₁ = (f /^ j) . b₁ )
assume that
A7: 1 <= k and
A8: k <= len (<*(f /. i)*> ^ (f /^ i)) ; :: thesis: (<*(f /. i)*> ^ (f /^ i)) . b₁ = (f /^ j) . b₁
A9: k in dom (f /^ j) by A6, A7, A8, FINSEQ_3:25;

per cases ( k = 1 or k <> 1 ) ;

suppose A10: k = 1 ; :: thesis: (<*(f /. i)*> ^ (f /^ i)) . b₁ = (f /^ j) . b₁

hence (<*(f /. i)*> ^ (f /^ i)) . k = f /. i by FINSEQ_1:41
.= f . i by A2, PARTFUN1:def 6
.= (f /^ j) . k by A1, A4, A9, A10, RFINSEQ:def 1 ;
:: thesis: verum

end;

suppose k <> 1 ; :: thesis: (<*(f /. i)*> ^ (f /^ i)) . b₁ = (f /^ j) . b₁

then A11: 1 < k by A7, XXREAL_0:1;
reconsider k9 = k - 1 as Element of NAT by A7, INT_1:5;
A12: k9 <= (len (<*(f /. i)*> ^ (f /^ i))) - 1 by A8, XREAL_1:9;
k9 + 1 = k ;
then 1 <= k9 by A11, NAT_1:13;
then A13: k9 in dom (f /^ i) by A5, A12, FINSEQ_3:25;
len <*(f /. i)*> = 1 by FINSEQ_1:39;
hence (<*(f /. i)*> ^ (f /^ i)) . k = (f /^ i) . k9 by A8, A11, FINSEQ_1:24
.= f . (k9 + i) by A3, A13, RFINSEQ:def 1
.= f . (k + j) by A1
.= (f /^ j) . k by A4, A9, RFINSEQ:def 1 ;
:: thesis: verum

end;

end;

end;

hence <*(f /. i)*> ^ (f /^ i) = f /^ j by A6; :: thesis: verum