let j, i 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:27;
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 2
.= (len f) - j by A1
.= len (f /^ j) by A4, RFINSEQ:def 2 ;

now

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:27;

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:58
.= f . i by A2, PARTFUN1:def 8
.= (f /^ j) . k by A1, A4, A9, A10, RFINSEQ:def 2 ;
:: 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 k' = k - 1 as Element of NAT by A7, INT_1:18;
k' + 1 = k ;
then A12: 1 <= k' by A11, NAT_1:13;
k' <= (len (<*(f /. i)*> ^ (f /^ i))) - 1 by A8, XREAL_1:11;
then A13: k' in dom (f /^ i) by A5, A12, FINSEQ_3:27;
len <*(f /. i)*> = 1 by FINSEQ_1:56;
hence (<*(f /. i)*> ^ (f /^ i)) . k = (f /^ i) . k' by A8, A11, FINSEQ_1:37
.= f . (k' + i) by A3, A13, RFINSEQ:def 2
.= f . (k + j) by A1
.= (f /^ j) . k by A4, A9, RFINSEQ:def 2 ;
:: thesis: verum

end;

end;

end;

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