defpred S_{1}[ 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_{1}[i,v]

A4: for i being Element of NAT holds S_{1}[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

( 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

proof

consider f being sequence of the carrier of L such that
let i be Element of NAT ; :: thesis: ex v being Element of L st S_{1}[i,v]

deffunc H_{1}( 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_{1}(k)
from FINSEQ_2:sch 1();

take v = Sum r; :: thesis: S_{1}[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;deffunc H

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

take v = Sum r; :: thesis: S

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

A4: for i being Element of NAT holds S

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