deffunc H₁( Nat) -> Element of the carrier of L = (p . ($1 -' 1)) * ((power L) . (x,($1 -' 1)));
consider F being FinSequence of the carrier of L such that
A1: len F = len p and
A2: for n being Nat st n in dom F holds
F . n = H₁(n) from FINSEQ_2:sch 1();
take y = Sum F; :: thesis: ex F being FinSequence of the carrier of L st
( y = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) )
take F ; :: thesis: ( y = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) )
thus ( y = Sum F & len F = len p ) by A1; :: thesis: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1)))
let n be Element of NAT ; :: thesis: ( n in dom F implies F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) )
assume n in dom F ; :: thesis: F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1)))
hence F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by A2; :: thesis: verum