let p, q be complex-valued FinSequence; :: thesis: ( len p = n & ( for i being Nat st 1 <= i & i <= n holds
for m being Nat st m = n - i holds
( ( i is odd implies p . i = r |^ m ) & ( i is even implies p . i = - (r |^ m) ) ) ) & len q = n & ( for i being Nat st 1 <= i & i <= n holds
for m being Nat st m = n - i holds
( ( i is odd implies q . i = r |^ m ) & ( i is even implies q . i = - (r |^ m) ) ) ) implies p = q )
assume that
A7: S₂[p] and
A8: S₂[q] ; :: thesis: p = q
thus len p = len q by A7, A8; :: 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 i be Nat; :: thesis: ( not 1 <= i or not i <= len p or p . i = q . i )
assume that
A9: 1 <= i and
A10: i <= len p ; :: thesis: p . i = q . i
reconsider m = n - i as Element of NAT by A7, A10, INT_1:5;

per cases ( i is odd or i is even ) ;

suppose A11: i is odd ; :: thesis: p . i = q . i

thus p . i = r |^ m by A7, A9, A10, A11
.= q . i by A7, A8, A9, A10, A11 ; :: thesis: verum

end;

suppose A12: i is even ; :: thesis: p . i = q . i

thus p . i = - (r |^ m) by A7, A9, A10, A12
.= q . i by A7, A8, A9, A10, A12 ; :: thesis: verum

end;

end;