let n be Nat; :: thesis: for c being Complex
for f being complex-valued FinSequence holds (c (#) f) | n = c (#) (f | n)
let c be Complex; :: thesis: for f being complex-valued FinSequence holds (c (#) f) | n = c (#) (f | n)
let f be complex-valued FinSequence; :: thesis: (c (#) f) | n = c (#) (f | n)
A1: len (c (#) f) = len f by COMPLSP2:3;
A2: len (c (#) (f | n)) = len (f | n) by COMPLSP2:3;

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

suppose A3: n <= len f ; :: thesis: (c (#) f) | n = c (#) (f | n)

then A4: len ((c (#) f) | n) = n by A1, FINSEQ_1:59;
hence len ((c (#) f) | n) = len (c (#) (f | n)) by A2, A3, FINSEQ_1:59; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len ((c (#) f) | n) or ((c (#) f) | n) . b₁ = (c (#) (f | n)) . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len ((c (#) f) | n) or ((c (#) f) | n) . k = (c (#) (f | n)) . k )
assume that
1 <= k and
A5: k <= len ((c (#) f) | n) ; :: thesis: ((c (#) f) | n) . k = (c (#) (f | n)) . k
A6: (f | n) . k = f . k by A4, A5, FINSEQ_3:112;
thus ((c (#) f) | n) . k = (c (#) f) . k by A4, A5, FINSEQ_3:112
.= c * (f . k) by VALUED_1:6
.= (c (#) (f | n)) . k by A6, VALUED_1:6 ; :: thesis: verum

end;

suppose A7: n > len f ; :: thesis: (c (#) f) | n = c (#) (f | n)

then A8: f | n = f by FINSEQ_1:58;
hence len ((c (#) f) | n) = len (c (#) (f | n)) by A2, A7, FINSEQ_1:58; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len ((c (#) f) | n) or ((c (#) f) | n) . b₁ = (c (#) (f | n)) . b₁ )
thus for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len ((c (#) f) | n) or ((c (#) f) | n) . b₁ = (c (#) (f | n)) . b₁ ) by A1, A7, A8, FINSEQ_1:58; :: thesis: verum

end;

end;