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 ]

proof

let f be complex-valued FinSequence; :: thesis: ( len f = 0 implies 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) ) ) ) )
assume A2: len f = 0 ; :: thesis: 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) ) ) )
take f ; :: thesis: ex o being complex-valued FinSequence st
( len f = [\((len f) / 2)/] & len o = [/((len f) / 2)\] & Sum f = (Sum f) + (Sum o) & ( for n being Nat holds
( f . n = f . (2 * n) & o . n = f . ((2 * n) - 1) ) ) )
take f ; :: thesis: ( len f = [\((len f) / 2)/] & len f = [/((len f) / 2)\] & Sum f = (Sum f) + (Sum f) & ( for n being Nat holds
( f . n = f . (2 * n) & f . n = f . ((2 * n) - 1) ) ) )
thus ( len f = [\((len f) / 2)/] & len f = [/((len f) / 2)\] ) by A2; :: thesis: ( Sum f = (Sum f) + (Sum f) & ( for n being Nat holds
( f . n = f . (2 * n) & f . n = f . ((2 * n) - 1) ) ) )
f = <*> REAL by A2;
hence Sum f = (Sum f) + (Sum f) by RVSUM_1:72; :: thesis: for n being Nat holds
( f . n = f . (2 * n) & f . n = f . ((2 * n) - 1) )
let n be Nat; :: thesis: ( f . n = f . (2 * n) & f . n = f . ((2 * n) - 1) )
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: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let f be complex-valued FinSequence; :: thesis: ( len f = n + 1 implies 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) ) ) ) )
assume A5: len f = n + 1 ; :: thesis: 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) ) ) )
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 ( n is even or n is odd ) ;

suppose n is even ; :: thesis: 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) ) ) )

then consider k being Nat such that
A10: 2 * k = n by ABIAN:def 2;
take e ; :: thesis: ex 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) ) ) )
take oF = o ^ <*(f . (n + 1))*>; :: thesis: ( len e = [\((len f) / 2)/] & len oF = [/((len f) / 2)\] & Sum f = (Sum e) + (Sum oF) & ( for n being Nat holds
( e . n = f . (2 * n) & oF . n = f . ((2 * n) - 1) ) ) )
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, Lm1, Lm2;
hence ( len e = [\((len f) / 2)/] & len oF = [/((len f) / 2)\] ) by FINSEQ_2:16, A5, A7; :: thesis: ( Sum f = (Sum e) + (Sum oF) & ( for n being Nat holds
( e . n = f . (2 * n) & oF . n = f . ((2 * n) - 1) ) ) )
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: for n being Nat holds
( e . n = f . (2 * n) & oF . n = f . ((2 * n) - 1) )
let i be Nat; :: thesis: ( e . i = f . (2 * i) & oF . i = f . ((2 * i) - 1) )
thus e . i = f . (2 * i) :: thesis: oF . i = f . ((2 * i) - 1)

proof

per cases ( 2 * i <= n or 2 * i > n ) ;

suppose 2 * i <= n ; :: thesis: e . i = f . (2 * i)

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

end;

suppose 2 * i > n ; :: thesis: e . i = f . (2 * i)

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: verum

end;

end;

end;

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

proof

per cases ( i = 0 or ( i <> 0 & 2 * i <= n ) or 2 * i > n ) ;

suppose i = 0 ; :: thesis: oF . i = f . ((2 * i) - 1)

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: verum

end;

suppose A14: ( i <> 0 & 2 * i <= n ) ; :: thesis: oF . i = f . ((2 * i) - 1)

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: verum

end;

suppose 2 * i > n ; :: thesis: oF . i = f . ((2 * i) - 1)

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 ( (2 * i) - 1 = len f or (2 * i) - 1 > len f ) by A16, XXREAL_0:1;

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

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

end;

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

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: verum

end;

end;

end;

end;

end;

end;

suppose n is odd ; :: thesis: 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) ) ) )

then consider k being Nat such that
A19: n = (2 * k) + 1 by ABIAN:9;
take eF = e ^ <*(f . (n + 1))*>; :: thesis: ex o being complex-valued FinSequence st
( len eF = [\((len f) / 2)/] & len o = [/((len f) / 2)\] & Sum f = (Sum eF) + (Sum o) & ( for n being Nat holds
( eF . n = f . (2 * n) & o . n = f . ((2 * n) - 1) ) ) )
take o ; :: thesis: ( len eF = [\((len f) / 2)/] & len o = [/((len f) / 2)\] & Sum f = (Sum eF) + (Sum o) & ( for n being Nat holds
( eF . n = f . (2 * n) & o . n = f . ((2 * n) - 1) ) ) )
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, Lm1, Lm2;
hence ( len eF = [\((len f) / 2)/] & len o = [/((len f) / 2)\] ) by FINSEQ_2:16, A5, A7; :: thesis: ( Sum f = (Sum eF) + (Sum o) & ( for n being Nat holds
( eF . n = f . (2 * n) & o . n = f . ((2 * n) - 1) ) ) )
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: for n being Nat holds
( eF . n = f . (2 * n) & o . n = f . ((2 * n) - 1) )
let i be Nat; :: thesis: ( eF . i = f . (2 * i) & o . i = f . ((2 * i) - 1) )
thus eF . i = f . (2 * i) :: thesis: o . i = f . ((2 * i) - 1)

proof

per cases ( i = 0 or ( i <> 0 & i <= k ) or i > k ) ;

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

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

end;

suppose ( i <> 0 & i <= k ) ; :: thesis: eF . i = f . (2 * i)

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: verum

end;

suppose i > k ; :: thesis: eF . i = f . (2 * i)

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

per cases ( i = k + 1 or i > k + 1 ) by A22, XXREAL_0:1;

suppose i = k + 1 ; :: thesis: eF . i = f . (2 * i)

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

end;

suppose A23: i > k + 1 ; :: thesis: eF . i = f . (2 * i)

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: verum

end;

end;

end;

end;

end;

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

proof

per cases ( i = 0 or ( i <> 0 & (2 * i) - 1 <= n ) or (2 * i) - 1 > n ) ;

suppose i = 0 ; :: thesis: o . i = f . ((2 * i) - 1)

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: verum

end;

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

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

end;

suppose (2 * i) - 1 > n ; :: thesis: o . i = f . ((2 * i) - 1)

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: verum

end;

end;

end;

end;

end;

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: verum