defpred S1[ 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 S1[i,v]
proof
let i be Element of NAT ; :: thesis: ex v being Element of L st S1[i,v]
deffunc H1( 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 = H1(k) from take v = Sum r; :: thesis: S1[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 sequence of the carrier of L such that
A4: for i being Element of NAT holds S1[i,f . i] from 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