let p be FinSequence; :: thesis: for i being Nat st i + 1 <= len p holds
p /^ i = <*(p . (i + 1))*> ^ (p /^ (i + 1))
let i be Nat; :: thesis: ( i + 1 <= len p implies p /^ i = <*(p . (i + 1))*> ^ (p /^ (i + 1)) )
assume A1: i + 1 <= len p ; :: thesis: 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; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (p /^ i) or (p /^ i) . b₁ = (<*(p . (i + 1))*> ^ (p /^ (i + 1))) . b₁ )
let j be Nat; :: thesis: ( 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) ) ; :: thesis: (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 A6: j = 1 ; :: thesis: (p /^ i) . j = (<*(p . (i + 1))*> ^ (p /^ (i + 1))) . j

hence (p /^ i) . j = p . (i + 1) by A2, A5, RFINSEQ:def 1
.= (<*(p . (i + 1))*> ^ (p /^ (i + 1))) . j by A6, FINSEQ_1:41 ;
:: thesis: verum

end;

suppose j > 1 ; :: thesis: (p /^ i) . j = (<*(p . (i + 1))*> ^ (p /^ (i + 1))) . j

then 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 ; :: thesis: verum

end;

end;