let f be complex-valued FinSequence; :: thesis: for i being Nat st i + 1 <= len f holds
(f | i) ^ <*(f . (i + 1))*> = f | (i + 1)
let i be Nat; :: thesis: ( i + 1 <= len f implies (f | i) ^ <*(f . (i + 1))*> = f | (i + 1) )
assume A1: i + 1 <= len f ; :: thesis: (f | i) ^ <*(f . (i + 1))*> = f | (i + 1)
set f1 = (f | i) ^ <*(f . (i + 1))*>;
set f2 = f | (i + 1);
A2: i <= i + 1 by NAT_1:11;
reconsider f1 = (f | i) ^ <*(f . (i + 1))*> as complex-valued FinSequence ;
A3: len f1 = (len (f | i)) + (len <*(f . (i + 1))*>) by FINSEQ_1:22
.= (len (f | i)) + 1 by FINSEQ_1:39
.= i + 1 by A1, A2, FINSEQ_1:59, XXREAL_0:2
.= len (f | (i + 1)) by A1, FINSEQ_1:59 ;
then A4: dom f1 = Seg (len (f | (i + 1))) by FINSEQ_1:def 3
.= dom (f | (i + 1)) by FINSEQ_1:def 3 ;
A5: i <= len f by A1, A2, XXREAL_0:2;

now :: thesis: for x9 being object st x9 in dom f1 holds
f1 . x9 = (f | (i + 1)) . x9

let x9 be object ; :: thesis: ( x9 in dom f1 implies f1 . b₁ = (f | (i + 1)) . b₁ )
assume A6: x9 in dom f1 ; :: thesis: f1 . b₁ = (f | (i + 1)) . b₁
then reconsider x = x9 as Element of NAT ;
A7: dom f1 = Seg (len f1) by FINSEQ_1:def 3;
then A8: 1 <= x by A6, FINSEQ_1:1;
x <= len f1 by A6, A7, FINSEQ_1:1;
then A9: x <= i + 1 by A1, A3, FINSEQ_1:59;

per cases ( x = i + 1 or x < i + 1 ) by A9, XXREAL_0:1;

suppose A10: x = i + 1 ; :: thesis: f1 . b₁ = (f | (i + 1)) . b₁

then x in Seg (i + 1) by A8;
then A11: x in dom (f | (i + 1)) by A1, FINSEQ_1:17;
dom <*(f . (i + 1))*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A12: 1 in dom <*(f . (i + 1))*> by TARSKI:def 1;
len (f | i) = i by A1, A2, FINSEQ_1:59, XXREAL_0:2;
hence f1 . x9 = <*(f . (i + 1))*> . 1 by A10, A12, FINSEQ_1:def 7
.= f . (i + 1)
.= (f | (i + 1)) . x9 by A10, A11, FUNCT_1:47 ;
:: thesis: verum

end;

suppose x < i + 1 ; :: thesis: f1 . b₁ = (f | (i + 1)) . b₁

then A13: x <= i by NAT_1:13;
1 <= x by A6, A7, FINSEQ_1:1;
then x in Seg i by A13;
then A14: x in dom (f | i) by A5, FINSEQ_1:17;
hence f1 . x9 = (f | i) . x by FINSEQ_1:def 7
.= f . x by A14, FUNCT_1:47
.= (f | (i + 1)) . x9 by A4, A6, FUNCT_1:47 ;
:: thesis: verum

end;

end;

end;

hence (f | i) ^ <*(f . (i + 1))*> = f | (i + 1) by A4; :: thesis: verum