let y1, y2 be Element of B; :: thesis: ( ex F being FinSequence of B st
( y1 = 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))) ) ) & ex F being FinSequence of B st
( y2 = 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))) ) ) implies y1 = y2 )
given F1 being FinSequence of B such that A3: y1 = Sum F1 and
A4: len F1 = len p and
A5: for n being Element of NAT st n in dom F1 holds
F1 . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ; :: thesis: ( for F being FinSequence of B holds
( not y2 = Sum F or not len F = len p or ex n being Element of NAT st
( n in dom F & not F . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ) ) or y1 = y2 )
given F2 being FinSequence of B such that A6: y2 = Sum F2 and
A7: len F2 = len p and
A8: for n being Element of NAT st n in dom F2 holds
F2 . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) ; :: thesis: y1 = y2
A9: dom F1 = Seg (len p) by A4, FINSEQ_1:def 3;

now :: thesis: for n being Nat st n in dom F1 holds
F1 . n = F2 . n

let n be Nat; :: thesis: ( n in dom F1 implies F1 . n = F2 . n )
assume A10: n in dom F1 ; :: thesis: F1 . n = F2 . n
then A11: n in dom F2 by A7, A9, FINSEQ_1:def 3;
thus F1 . n = (In ((p . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) by A5, A10
.= F2 . n by A8, A11 ; :: thesis: verum

end;

hence y1 = y2 by A3, A4, A6, A7, FINSEQ_2:9; :: thesis: verum