let p, q be FinSequence of REAL ; :: thesis: ( len p = n & ( for i being Nat st 1 <= i & i <= n holds
p . i = (b + i) to_power e ) & len q = n & ( for i being Nat st 1 <= i & i <= n holds
q . i = (b + i) to_power e ) implies p = q )
assume that
A3: len p = n and
A4: for i being Nat st 1 <= i & i <= n holds
p . i = (b + i) to_power e and
A5: len q = n and
A6: for i being Nat st 1 <= i & i <= n holds
q . i = (b + i) to_power e ; :: thesis: p = q
thus len p = len q by A3, A5; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len p or p . b₁ = q . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len p or p . k = q . k )
assume A7: ( 1 <= k & k <= len p ) ; :: thesis: p . k = q . k
thus p . k = (b + k) to_power e by A3, A4, A7
.= q . k by A3, A6, A7 ; :: thesis: verum