let i, j be Nat; 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 ; 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; ( 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
; <*(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 for k being Nat st 1 <= k & k <= len (<*(f /. i)*> ^ (f /^ i)) holds
(<*(f /. i)*> ^ (f /^ i)) . k = (f /^ j) . klet k be
Nat;
( 1 <= k & k <= len (<*(f /. i)*> ^ (f /^ i)) implies (<*(f /. i)*> ^ (f /^ i)) . b1 = (f /^ j) . b1 )assume that A7:
1
<= k
and A8:
k <= len (<*(f /. i)*> ^ (f /^ i))
;
(<*(f /. i)*> ^ (f /^ i)) . b1 = (f /^ j) . b1A9:
k in dom (f /^ j)
by A6, A7, A8, FINSEQ_3:25;
per cases
( k = 1 or k <> 1 )
;
suppose
k <> 1
;
(<*(f /. i)*> ^ (f /^ i)) . b1 = (f /^ j) . b1then 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
;
verum end; end; end;
hence
<*(f /. i)*> ^ (f /^ i) = f /^ j
by A6; verum