A1: for k being Nat st k in Seg n holds
ex x being Element of COMPLEX st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg n implies ex x being Element of COMPLEX st S₁[k,x] )
assume A2: k in Seg n ; :: thesis: ex x being Element of COMPLEX st S₁[k,x]
k <= n by A2, FINSEQ_1:1;
then reconsider m = n - k as Element of NAT by INT_1:5;

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

suppose A3: k is odd ; :: thesis: ex x being Element of COMPLEX st S₁[k,x]

reconsider x = r |^ m as Element of COMPLEX by XCMPLX_0:def 2;
take x ; :: thesis: S₁[k,x]
thus S₁[k,x] by A3; :: thesis: verum

end;

suppose A4: k is even ; :: thesis: ex x being Element of COMPLEX st S₁[k,x]

reconsider x = - (r |^ m) as Element of COMPLEX by XCMPLX_0:def 2;
take x ; :: thesis: S₁[k,x]
thus S₁[k,x] by A4; :: thesis: verum

end;

end;

end;

consider p being FinSequence of COMPLEX such that
A5: dom p = Seg n and
A6: for k being Nat st k in Seg n holds
S₁[k,p . k] from FINSEQ_1:sch 5(A1);
take p ; :: 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) ) ) ) )
n in NAT by ORDINAL1:def 12;
hence len p = n by A5, FINSEQ_1:def 3; :: thesis: 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) ) )
let i be Nat; :: thesis: ( 1 <= i & i <= n implies 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) ) ) )
assume ( 1 <= i & i <= n ) ; :: thesis: 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) ) )
then i in Seg n ;
hence 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) ) ) by A6; :: thesis: verum