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]

let i be Element of NAT ; :: thesis:
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:
take r ; :: thesis:
thus len r = i + 1 by A2; :: thesis:
thus v = Sum r ; :: thesis:
let k be Element of NAT ; :: thesis:
assume k in dom r ; :: thesis:
hence r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A3; :: thesis:

end;

consider f being sequence of 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:
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: