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