let p be FinSequence; for i being Nat st i + 1 <= len p holds
p /^ i = <*(p . (i + 1))*> ^ (p /^ (i + 1))
let i be Nat; ( i + 1 <= len p implies p /^ i = <*(p . (i + 1))*> ^ (p /^ (i + 1)) )
assume A1:
i + 1 <= len p
; p /^ i = <*(p . (i + 1))*> ^ (p /^ (i + 1))
then A2:
i < len p
by NAT_1:13;
then A3:
len (p /^ i) = (len p) - i
by RFINSEQ:def 1;
len (<*(p . (i + 1))*> ^ (p /^ (i + 1))) =
(len <*(p . (i + 1))*>) + (len (p /^ (i + 1)))
by FINSEQ_1:22
.=
1 + (len (p /^ (i + 1)))
by FINSEQ_1:40
.=
1 + ((len p) - (i + 1))
by A1, RFINSEQ:def 1
.=
(len p) - i
;
hence
len (p /^ i) = len (<*(p . (i + 1))*> ^ (p /^ (i + 1)))
by A2, RFINSEQ:def 1; FINSEQ_1:def 17 for b1 being set holds
( not 1 <= b1 or not b1 <= len (p /^ i) or (p /^ i) . b1 = (<*(p . (i + 1))*> ^ (p /^ (i + 1))) . b1 )
let j be Nat; ( not 1 <= j or not j <= len (p /^ i) or (p /^ i) . j = (<*(p . (i + 1))*> ^ (p /^ (i + 1))) . j )
assume A4:
( 1 <= j & j <= len (p /^ i) )
; (p /^ i) . j = (<*(p . (i + 1))*> ^ (p /^ (i + 1))) . j
then A5:
j in dom (p /^ i)
by FINSEQ_3:25;
per cases
( j = 1 or j > 1 )
by A4, XXREAL_0:1;
suppose
j > 1
;
(p /^ i) . j = (<*(p . (i + 1))*> ^ (p /^ (i + 1))) . jthen
j >= 1
+ 1
by NAT_1:13;
then consider k being
Nat such that A7:
j = (1 + 1) + k
by NAT_1:10;
A8:
len <*(p . (i + 1))*> = 1
by FINSEQ_1:40;
A9:
(
len (p /^ (i + 1)) = (len p) - (i + 1) &
((len p) - (i + 1)) + 1
= (len p) - i &
j = (1 + k) + 1 )
by A1, A7, RFINSEQ:def 1;
then
( 1
<= 1
+ k & 1
+ k <= len (p /^ (i + 1)) )
by A3, A4, XREAL_1:6, NAT_1:11;
then A10:
1
+ k in dom (p /^ (i + 1))
by FINSEQ_3:25;
thus (p /^ i) . j =
p . (i + j)
by A2, A5, RFINSEQ:def 1
.=
p . ((i + 1) + (1 + k))
by A7
.=
(p /^ (i + 1)) . (1 + k)
by A1, A10, RFINSEQ:def 1
.=
(<*(p . (i + 1))*> ^ (p /^ (i + 1))) . j
by A8, A10, A9, FINSEQ_1:def 7
;
verum end;