defpred S₁[ Nat] means for f being complex-valued FinSequence st len f = $1 holds
ex e, o being complex-valued FinSequence st
( len e = [\((len f) / 2)/] & len o = [/((len f) / 2)\] & Sum f = (Sum e) + (Sum o) & ( for n being Nat holds
( e . n = f . (2 * n) & o . n = f . ((2 * n) - 1) ) ) );
A1: S₁[ 0 ]

let f be complex-valued FinSequence; :: thesis:
assume A2: len f = 0 ; :: thesis:
take f ; :: thesis:
take f ; :: thesis:
thus ( len f = [\((len f) / 2)/] & len f = [/((len f) / 2)\] ) by A2, INT_1:25, INT_1:30; :: thesis:
f = <*> REAL by A2;
hence Sum f = (Sum f) + (Sum f) by RVSUM_1:72; :: thesis:
let n be Nat; :: thesis:
f = {} by A2;
then ( f . n = 0 & 0 = f . (2 * n) & f . n = 0 & 0 = f . ((2 * n) - 1) ) ;
hence ( f . n = f . (2 * n) & f . n = f . ((2 * n) - 1) ) ; :: thesis:

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A4: S₁[n] ; :: thesis:
set n1 = n + 1;
let f be complex-valued FinSequence; :: thesis:
assume A5: len f = n + 1 ; :: thesis:
set fn = f | n;
A6: f = (f | n) ^ <*(f . (n + 1))*> by A5, FINSEQ_3:55;
n < n + 1 by NAT_1:13;
then len (f | n) = n by A5, FINSEQ_1:59;
then consider e, o being complex-valued FinSequence such that
A7: ( len e = [\(n / 2)/] & len o = [/(n / 2)\] ) and
A8: Sum (f | n) = (Sum e) + (Sum o) and
A9: for k being Nat holds
( e . k = (f | n) . (2 * k) & o . k = (f | n) . ((2 * k) - 1) ) by A4;

per cases ;

suppose n is even ; :: thesis:

then consider k being Nat such that
A10: 2 * k = n by ABIAN:def 2;
take e ; :: thesis:
take oF = o ^ <*(f . (n + 1))*>; :: thesis:
A11: len oF = (len o) + 1 by FINSEQ_2:16;
A12: ( [\(n / 2)/] = k & k = [\((n + 1) / 2)/] & [/(n / 2)\] = k & [/((n + 1) / 2)\] = k + 1 ) by A10, INT_1:25, INT_1:30, Lm1, Lm2;
hence ( len e = [\((len f) / 2)/] & len oF = [/((len f) / 2)\] ) by FINSEQ_2:16, A5, A7; :: thesis:
thus Sum f = (Sum (f | n)) + (f . (n + 1)) by A6, RVSUM_2:31
.= (Sum e) + ((Sum o) + (f . (n + 1))) by A8
.= (Sum e) + (Sum oF) by RVSUM_2:31 ; :: thesis:
let i be Nat; :: thesis:
thus e . i = f . (2 * i) :: thesis:

proof

per cases ;

suppose 2 * i <= n ; :: thesis:

then (f | n) . (2 * i) = f . (2 * i) by FINSEQ_3:112;
hence e . i = f . (2 * i) by A9; :: thesis:

end;

suppose 2 * i > n ; :: thesis:

then A13: i > k by A10, XREAL_1:64;
then i >= k + 1 by NAT_1:13;
then ( 2 * i >= 2 * (k + 1) & 2 * (k + 1) = (len f) + 1 ) by A10, A5, XREAL_1:64;
then 2 * i > len f by NAT_1:13;
then ( not 2 * i in dom f & not i in dom e ) by FINSEQ_3:25, A7, A12, A13;
then ( f . (2 * i) = 0 & 0 = e . i ) by FUNCT_1:def 2;
hence e . i = f . (2 * i) ; :: thesis:

end;

thus oF . i = f . ((2 * i) - 1) :: thesis:

proof

per cases ;

suppose i = 0 ; :: thesis:

then ( not i in dom oF & not (2 * i) - 1 in dom f ) by FINSEQ_3:25;
then ( oF . i = 0 & 0 = f . ((2 * i) - 1) ) by FUNCT_1:def 2;
hence oF . i = f . ((2 * i) - 1) ; :: thesis:

end;

suppose A14: ( i <> 0 & 2 * i <= n ) ; :: thesis:

then ( 1 <= i & i <= k ) by A10, XREAL_1:68, NAT_1:14;
then i in dom o by A7, A12, FINSEQ_3:25;
then A15: oF . i = o . i by FINSEQ_1:def 7
.= (f | n) . ((2 * i) - 1) by A9 ;
(2 * i) - 1 <= n - 0 by XREAL_1:13, A14;
hence oF . i = f . ((2 * i) - 1) by A15, A14, FINSEQ_3:112; :: thesis:

end;

suppose 2 * i > n ; :: thesis:

then i > k by A10, XREAL_1:64;
then i >= k + 1 by NAT_1:13;
then ( 2 * i >= 2 * (k + 1) & 2 * (k + 1) = (len f) + 1 ) by A10, A5, XREAL_1:64;
then A16: (2 * i) - 1 >= len f by XREAL_1:19;

per cases ) - 1 = len f or (2 * i) - 1 > len f ) by A16, XXREAL_0:1;

suppose (2 * i) - 1 = len f ; :: thesis:

hence oF . i = f . ((2 * i) - 1) by A5, A10, A7, A12; :: thesis:

end;

suppose A17: (2 * i) - 1 > len f ; :: thesis:

then not (2 * i) - 1 in dom f by FINSEQ_3:25;
then A18: f . ((2 * i) - 1) = 0 by FUNCT_1:def 2;
2 * i > (len f) + 1 by A17, XREAL_1:20;
then 2 * i > 2 * (k + 1) by A10, A5;
then i > k + 1 by XREAL_1:64;
then not i in dom oF by A11, A12, A7, FINSEQ_3:25;
hence oF . i = f . ((2 * i) - 1) by A18, FUNCT_1:def 2; :: thesis:

end;

suppose n is odd ; :: thesis:

then consider k being Nat such that
A19: n = (2 * k) + 1 by ABIAN:9;
take eF = e ^ <*(f . (n + 1))*>; :: thesis:
take o ; :: thesis:
A20: len eF = (len e) + 1 by FINSEQ_2:16;
A21: ( [\(n / 2)/] = k & [\((n + 1) / 2)/] = k + 1 & [/(n / 2)\] = k + 1 & [/((n + 1) / 2)\] = k + 1 ) by A19, INT_1:25, INT_1:30, Lm1, Lm2;
hence ( len eF = [\((len f) / 2)/] & len o = [/((len f) / 2)\] ) by FINSEQ_2:16, A5, A7; :: thesis:
thus Sum f = (Sum (f | n)) + (f . (n + 1)) by A6, RVSUM_2:31
.= ((Sum e) + (f . (n + 1))) + (Sum o) by A8
.= (Sum eF) + (Sum o) by RVSUM_2:31 ; :: thesis:
let i be Nat; :: thesis:
thus eF . i = f . (2 * i) :: thesis:

proof

per cases ;

suppose i = 0 ; :: thesis:

hence eF . i = f . (2 * i) ; :: thesis:

end;

suppose ( i <> 0 & i <= k ) ; :: thesis:

then ( 1 <= i & i <= k & 2 * i <= 2 * k ) by NAT_1:14, XREAL_1:64;
then ( i in dom e & 2 * i < n ) by A19, NAT_1:13, FINSEQ_3:25, A7, A21;
then ( eF . i = e . i & (f | n) . (2 * i) = f . (2 * i) ) by FINSEQ_1:def 7, FINSEQ_3:112;
hence eF . i = f . (2 * i) by A9; :: thesis:

end;

suppose i > k ; :: thesis:

then A22: i >= k + 1 by NAT_1:13;

per cases by A22, XXREAL_0:1;

suppose i = k + 1 ; :: thesis:

hence eF . i = f . (2 * i) by A19, A7, A21; :: thesis:

end;

suppose A23: i > k + 1 ; :: thesis:

then not i in dom eF by FINSEQ_3:25, A7, A20, A21;
then A24: eF . i = 0 by FUNCT_1:def 2;
2 * i > 2 * (k + 1) by A23, XREAL_1:68;
then not 2 * i in dom f by A5, A19, FINSEQ_3:25;
hence eF . i = f . (2 * i) by A24, FUNCT_1:def 2; :: thesis:

end;

thus o . i = f . ((2 * i) - 1) :: thesis:

proof

per cases ;

suppose i = 0 ; :: thesis:

then ( not i in dom o & not (2 * i) - 1 in dom f ) by FINSEQ_3:25;
then ( o . i = 0 & 0 = f . ((2 * i) - 1) ) by FUNCT_1:def 2;
hence o . i = f . ((2 * i) - 1) ; :: thesis:

end;

suppose A25: ( i <> 0 & (2 * i) - 1 <= n ) ; :: thesis:

(f | n) . ((2 * i) - 1) = f . ((2 * i) - 1) by A25, FINSEQ_3:112;
hence o . i = f . ((2 * i) - 1) by A9; :: thesis:

end;

suppose (2 * i) - 1 > n ; :: thesis:

then 2 * i > n + 1 by XREAL_1:20;
then 2 * i > 2 * (k + 1) by A19;
then A26: i > k + 1 by XREAL_1:64;
then not i in dom o by FINSEQ_3:25, A7, A21;
then A27: o . i = 0 by FUNCT_1:def 2;
i >= (k + 1) + 1 by A26, NAT_1:13;
then 2 * i >= 2 * ((k + 1) + 1) by XREAL_1:64;
then 2 * i >= ((len f) + 1) + 1 by A19, A5;
then 2 * i > (len f) + 1 by NAT_1:13;
then not (2 * i) - 1 in dom f by XREAL_1:20, FINSEQ_3:25;
hence o . i = f . ((2 * i) - 1) by A27, FUNCT_1:def 2; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence for f being complex-valued FinSequence ex e, o being complex-valued FinSequence st
( len e = [\((len f) / 2)/] & len o = [/((len f) / 2)\] & Sum f = (Sum e) + (Sum o) & ( for n being Nat holds
( e . n = f . (2 * n) & o . n = f . ((2 * n) - 1) ) ) ) ; :: thesis: