defpred S₁[ Nat, set ] means $2 = (p . ($1 -' 1)) * (q `^ ($1 -' 1));
set k = len p;

A1: now :: thesis: for n being Nat st n in Seg (len p) holds
ex x being Element of (Polynom-Ring L) st S₁[n,x]

let n be Nat; :: thesis: ( n in Seg (len p) implies ex x being Element of (Polynom-Ring L) st S₁[n,x] )
assume n in Seg (len p) ; :: thesis: ex x being Element of (Polynom-Ring L) st S₁[n,x]
reconsider x = (p . (n -' 1)) * (q `^ (n -' 1)) as Element of (Polynom-Ring L) by POLYNOM3:def 10;
take x = x; :: thesis: S₁[n,x]
thus S₁[n,x] ; :: thesis: verum

end;

consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A2: ( dom F = Seg (len p) & ( for n being Nat st n in Seg (len p) holds
S₁[n,F . n] ) ) from FINSEQ_1:sch 5(A1);
reconsider r = Sum F as Polynomial of L by POLYNOM3:def 10;
take r ; :: thesis: ex F being FinSequence of the carrier of (Polynom-Ring L) st
( r = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) )
take F ; :: thesis: ( r = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) )
thus ( r = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) by A2, FINSEQ_1:def 3; :: thesis: verum