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
.= len (f | (i + 1)) by ;
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 ;
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 . b1 = (f | (i + 1)) . b1 )
assume A6: x9 in dom f1 ; :: thesis: f1 . b1 = (f | (i + 1)) . b1
then reconsider x = x9 as Element of NAT ;
A7: dom f1 = Seg (len f1) by FINSEQ_1:def 3;
then A8: 1 <= x by ;
x <= len f1 by ;
then A9: x <= i + 1 by ;
per cases ( x = i + 1 or x < i + 1 ) by ;
suppose A10: x = i + 1 ; :: thesis: f1 . b1 = (f | (i + 1)) . b1
then x in Seg (i + 1) by A8;
then A11: x in dom (f | (i + 1)) by ;
dom <*(f . (i + 1))*> = {1} by ;
then A12: 1 in dom <*(f . (i + 1))*> by TARSKI:def 1;
len (f | i) = i by ;
hence f1 . x9 = <*(f . (i + 1))*> . 1 by
.= f . (i + 1) by FINSEQ_1:40
.= (f | (i + 1)) . x9 by ;
:: thesis: verum
end;
suppose x < i + 1 ; :: thesis: f1 . b1 = (f | (i + 1)) . b1
then A13: x <= i by NAT_1:13;
1 <= x by ;
then x in Seg i by A13;
then A14: x in dom (f | i) by ;
hence f1 . x9 = (f | i) . x by FINSEQ_1:def 7
.= f . x by
.= (f | (i + 1)) . x9 by ;
:: thesis: verum
end;
end;
end;
hence (f | i) ^ <*(f . (i + 1))*> = f | (i + 1) by A4; :: thesis: verum