defpred S₁[ Element of NAT , Element of L] means ex r being FinSequence of the carrier of L st
( len r = $1 + 1 & $2 = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . (($1 + 1) -' k)) ) );
A1: for i being Element of NAT ex v being Element of L st S₁[i,v]

proof

let i be Element of NAT ; :: thesis: ex v being Element of L st S₁[i,v]
deffunc H₁( Nat) -> Element of the carrier of L = (p . ($1 -' 1)) * (q . ((i + 1) -' $1));
consider r being FinSequence of the carrier of L such that
A2: len r = i + 1 and
A3: for k being Nat st k in dom r holds
r . k = H₁(k) from FINSEQ_2:sch 1();
take v = Sum r; :: thesis: S₁[i,v]
take r ; :: thesis: ( len r = i + 1 & v = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )
thus len r = i + 1 by A2; :: thesis: ( v = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )
thus v = Sum r ; :: thesis: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k))
let k be Element of NAT ; :: thesis: ( k in dom r implies r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) )
assume k in dom r ; :: thesis: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k))
hence r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A3; :: thesis: verum

end;

consider f being Function of NAT, the carrier of L such that
A4: for i being Element of NAT holds S₁[i,f . i] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & f . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )
thus for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & f . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) by A4; :: thesis: verum