<%(- c),(1. L)%> is Element of (Polynom-Ring L) by POLYNOM3:def 10;
then reconsider f = n |-> <%(- c),(1. L)%> as FinSequence of (Polynom-Ring L) by FINSEQ_2:63;
take f ; :: thesis: ( len f = n & ( for i being Element of NAT st i in dom f holds
f . i = <%(- c),(1. L)%> ) )
thus A1: len f = n by CARD_1:def 7; :: thesis: for i being Element of NAT st i in dom f holds
f . i = <%(- c),(1. L)%>
let i be Element of NAT ; :: thesis: ( i in dom f implies f . i = <%(- c),(1. L)%> )
assume i in dom f ; :: thesis: f . i = <%(- c),(1. L)%>
then i in Seg n by A1, FINSEQ_1:def 3;
hence f . i = <%(- c),(1. L)%> by FUNCOP_1:7; :: thesis: verum