<%(- 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

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