let n be Nat; :: thesis: for f being complex-valued FinSequence holds (f | n) " = (f ") | n
let f be complex-valued FinSequence; :: thesis: (f | n) " = (f ") | n
A1: len (f ") = len f by Th55;

per cases ( n <= len f or len f < n ) ;

suppose A2: n <= len f ; :: thesis: (f | n) " = (f ") | n

then A3: len (f | n) = n by FINSEQ_1:59;
dom ((f | n) ") = dom (f | n) by VALUED_1:def 7
.= Seg (len ((f ") | n)) by A1, A2, A3, FINSEQ_1:59, FINSEQ_1:def 3
.= dom ((f ") | n) by FINSEQ_1:def 3 ;
hence len ((f | n) ") = len ((f ") | n) by FINSEQ_3:29; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len ((f | n) ") or ((f | n) ") . b₁ = ((f ") | n) . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len ((f | n) ") or ((f | n) ") . k = ((f ") | n) . k )
assume that
1 <= k and
A4: k <= len ((f | n) ") ; :: thesis: ((f | n) ") . k = ((f ") | n) . k
A5: len ((f | n) ") = len (f | n) by Th55;
then (f | n) . k = f . k by A3, A4, FINSEQ_3:112;
hence ((f | n) ") . k = (f . k) " by VALUED_1:10
.= (f ") . k by VALUED_1:10
.= ((f ") | n) . k by A3, A4, A5, FINSEQ_3:112 ;
:: thesis: verum

end;

suppose len f < n ; :: thesis: (f | n) " = (f ") | n

then ( f | n = f & (f ") | n = f " ) by A1, FINSEQ_1:58;
hence (f | n) " = (f ") | n ; :: thesis: verum

end;

end;