let n be Nat; :: thesis: for a being non trivial Nat ex Fy, Fx being FinSequence of NAT st
( Sum Fy = Py (a,n) & len Fy = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ n) + (Sum Fx) = Px (a,n) & len Fx = [\(n / 2)/] & ( for i being Nat st 1 <= i & i <= n / 2 holds
Fx . i = ((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
let a be non trivial Nat; :: thesis: ex Fy, Fx being FinSequence of NAT st
( Sum Fy = Py (a,n) & len Fy = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ n) + (Sum Fx) = Px (a,n) & len Fx = [\(n / 2)/] & ( for i being Nat st 1 <= i & i <= n / 2 holds
Fx . i = ((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
set A = (a ^2) -' 1;
defpred S₁[ Nat] means ex Fy, Fx being FinSequence of NAT st
( Sum Fy = Py (a,$1) & len Fy = [\(($1 + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= ($1 + 1) / 2 holds
Fy . i = (($1 choose ((2 * i) -' 1)) * (a |^ (($1 + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ $1) + (Sum Fx) = Px (a,$1) & len Fx = [\($1 / 2)/] & ( for i being Nat st 1 <= i & i <= $1 / 2 holds
Fx . i = (($1 choose (2 * i)) * (a |^ ($1 -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) );
A1: S₁[ 0 ]

proof

set F = <*> NAT;
A2: len (<*> NAT) = 0 ;
A3: 0 = [\(((0 * 2) + 1) / 2)/] by Lm1;
A4: for i being Nat st 1 <= i & i <= (0 + 1) / 2 holds
(<*> NAT) . i = ((0 choose ((2 * i) -' 1)) * (a |^ ((0 + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by XXREAL_0:2;
A5: Sum (<*> NAT) = Py (a,0) by Th6;
a |^ 0 = 1 by NEWTON:4;
then A6: (a |^ 0) + (Sum (<*> NAT)) = Px (a,0) by Th6;
for i being Nat st 1 <= i & i <= 0 / 2 holds
(<*> NAT) . i = ((0 choose (2 * i)) * (a |^ (0 -' (2 * i)))) * (((a ^2) -' 1) |^ i) ;
hence S₁[ 0 ] by A2, A3, A4, A5, A6; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set n1 = n + 1;
assume S₁[n] ; :: thesis: S₁[n + 1]
then consider Fy, Fx being FinSequence of NAT such that
A8: ( Sum Fy = Py (a,n) & len Fy = [\((n + 1) / 2)/] ) and
A9: for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) and
A10: ( (a |^ n) + (Sum Fx) = Px (a,n) & len Fx = [\(n / 2)/] ) and
A11: for i being Nat st 1 <= i & i <= n / 2 holds
Fx . i = ((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2) -' 1) |^ i) ;
set Fxa = <*(a |^ n)*> ^ Fx;
set Fx0 = Fx ^ <*0*>;
set Fy0 = Fy ^ <*0*>;
A12: Px (a,(n + 1)) = (((a |^ n) + (Sum Fx)) * a) + ((Sum Fy) * ((a ^2) -' 1)) by Th9, A8, A10
.= (((a |^ n) * a) + ((Sum Fx) * a)) + ((Sum Fy) * ((a ^2) -' 1))
.= ((a |^ (n + 1)) + ((Sum Fx) * a)) + ((Sum Fy) * ((a ^2) -' 1)) by NEWTON:6
.= ((a |^ (n + 1)) + (Sum (a * Fx))) + ((Sum Fy) * ((a ^2) -' 1)) by RVSUM_1:87 ;
A13: (Sum Fy) * ((a ^2) -' 1) = Sum (((a ^2) -' 1) * Fy) by RVSUM_1:87;
A14: Sum (Fy ^ <*0*>) = (Sum Fy) + 0 by RVSUM_1:74;
A15: Sum (Fx ^ <*0*>) = (Sum Fx) + 0 by RVSUM_1:74;
A16: Sum (a * (Fx ^ <*0*>)) = a * (Sum (Fx ^ <*0*>)) by RVSUM_1:87;
A17: Py (a,(n + 1)) = (Px (a,n)) + ((Py (a,n)) * a) by Th9
.= (Sum (<*(a |^ n)*> ^ Fx)) + ((Sum Fy) * a) by A8, A10, RVSUM_1:76 ;

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

suppose A18: n is odd ; :: thesis: S₁[n + 1]

then consider k being Nat such that
A19: n = (2 * k) + 1 by ABIAN:9;
set k1 = k + 1;
A20: ( [\((n + 1) / 2)/] = k + 1 & [\(n / 2)/] = k ) by A19, Lm1;
then A21: ( len (<*(a |^ n)*> ^ Fx) = k + 1 & len (a * Fy) = k + 1 ) by A10, FINSEQ_5:8, A8, RVSUM_1:117;
( rng (<*(a |^ n)*> ^ Fx) c= REAL & rng (a * Fy) c= REAL ) ;
then ( <*(a |^ n)*> ^ Fx is FinSequence of REAL & a * Fy is FinSequence of REAL ) by FINSEQ_1:def 4;
then reconsider FxA = <*(a |^ n)*> ^ Fx, aFy = a * Fy as Element of (k + 1) -tuples_on REAL by A21, FINSEQ_2:92;
rng ((<*(a |^ n)*> ^ Fx) + (a * Fy)) c= NAT by VALUED_0:def 6;
then reconsider FY = (<*(a |^ n)*> ^ Fx) + (a * Fy) as FinSequence of NAT by FINSEQ_1:def 4;
A22: ( len (a * (Fx ^ <*0*>)) = len (Fx ^ <*0*>) & len (Fx ^ <*0*>) = k + 1 & len (((a ^2) -' 1) * Fy) = k + 1 ) by A20, A8, A10, FINSEQ_2:16, RVSUM_1:117;
reconsider AFx0 = a * (Fx ^ <*0*>), AFy = ((a ^2) -' 1) * Fy as Element of (k + 1) -tuples_on REAL by A22, FINSEQ_2:92;
rng ((a * (Fx ^ <*0*>)) + (((a ^2) -' 1) * Fy)) c= NAT by VALUED_0:def 6;
then reconsider FX = (a * (Fx ^ <*0*>)) + (((a ^2) -' 1) * Fy) as FinSequence of NAT by FINSEQ_1:def 4;
take FY ; :: thesis: ex Fx being FinSequence of NAT st
( Sum FY = Py (a,(n + 1)) & len FY = [\(((n + 1) + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= ((n + 1) + 1) / 2 holds
FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ (n + 1)) + (Sum Fx) = Px (a,(n + 1)) & len Fx = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
Fx . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
take FX ; :: thesis: ( Sum FY = Py (a,(n + 1)) & len FY = [\(((n + 1) + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= ((n + 1) + 1) / 2 holds
FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ (n + 1)) + (Sum FX) = Px (a,(n + 1)) & len FX = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
thus Sum FY = (Sum FxA) + (Sum aFy) by RVSUM_1:89
.= Py (a,(n + 1)) by A17, RVSUM_1:87 ; :: thesis: ( len FY = [\(((n + 1) + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= ((n + 1) + 1) / 2 holds
FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ (n + 1)) + (Sum FX) = Px (a,(n + 1)) & len FX = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
A23: (n + 1) + 1 = (2 * (k + 1)) + 1 by A19;
len (FxA + aFy) = k + 1 by CARD_1:def 7;
hence len FY = [\(((n + 1) + 1) / 2)/] by A23, Lm1; :: thesis: ( ( for i being Nat st 1 <= i & i <= ((n + 1) + 1) / 2 holds
FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ (n + 1)) + (Sum FX) = Px (a,(n + 1)) & len FX = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
thus for i being Nat st 1 <= i & i <= ((n + 1) + 1) / 2 holds
FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) :: thesis: ( (a |^ (n + 1)) + (Sum FX) = Px (a,(n + 1)) & len FX = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )

proof

let i be Nat; :: thesis: ( 1 <= i & i <= ((n + 1) + 1) / 2 implies FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) )
assume A24: ( 1 <= i & i <= ((n + 1) + 1) / 2 ) ; :: thesis: FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))
set i1 = i -' 1;
A25: (i -' 1) + 1 = i by A24, XREAL_1:235;
2 * 1 <= 2 * i by A24, XREAL_1:66;
then A26: (2 * i) -' 1 = (2 * i) - 1 by XREAL_1:233, XXREAL_0:2;
A27: 2 * i <= (n + 1) + 1 by A24, XREAL_1:83;
then A28: 2 * i < (n + 1) + 1 by A18, XXREAL_0:1;
then A29: 2 * i <= n + 1 by NAT_1:13;
A30: i <= (n + 1) / 2 by A28, NAT_1:13, XREAL_1:77;
A31: (n + 1) -' (2 * i) = (n + 1) - (2 * i) by A29, XREAL_1:233;
A32: ((n + 1) + 1) -' (2 * i) = ((n + 1) + 1) - (2 * i) by XREAL_1:233, A27;
then A33: ((n + 1) + 1) -' (2 * i) = 1 + ((n + 1) -' (2 * i)) by A31;
Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A24, A9, A30;
then A34: (a * Fy) . i = a * (((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))) by VALUED_1:6
.= ((n choose ((2 * i) -' 1)) * (a * (a |^ ((n + 1) -' (2 * i))))) * (((a ^2) -' 1) |^ (i -' 1))
.= ((n choose ((2 * (i -' 1)) + 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A26, A25, A33, NEWTON:6 ;
2 * i <= (n + 1) + 1 by A24, XREAL_1:83;
then ((2 * (i -' 1)) + 1) + 1 <= (n + 1) + 1 by A25;
then (2 * (i -' 1)) + 1 <= n + 1 by XREAL_1:8;
then A35: 2 * (i -' 1) < n + 1 by NAT_1:13;
then A36: 2 * (i -' 1) <= n by NAT_1:13;
then A37: n -' (2 * (i -' 1)) = n - (2 * (i -' 1)) by XREAL_1:233;
A38: (<*(a |^ n)*> ^ Fx) . i = ((n choose (2 * (i -' 1))) * (a |^ (n -' (2 * (i -' 1))))) * (((a ^2) -' 1) |^ (i -' 1))

proof

per cases ( i > 1 or i <= 1 ) ;

suppose A39: i > 1 ; :: thesis: (<*(a |^ n)*> ^ Fx) . i = ((n choose (2 * (i -' 1))) * (a |^ (n -' (2 * (i -' 1))))) * (((a ^2) -' 1) |^ (i -' 1))

then A40: i -' 1 >= 1 by A25, NAT_1:13;
i -' 1 <= n / 2 by XREAL_1:77, A35, NAT_1:13;
then A41: Fx . (i -' 1) = ((n choose (2 * (i -' 1))) * (a |^ (n -' (2 * (i -' 1))))) * (((a ^2) -' 1) |^ (i -' 1)) by A11, A39, A25, NAT_1:13;
2 * (i -' 1) < (2 * k) + 1 by A36, A19, XXREAL_0:1;
then i -' 1 <= k by XREAL_1:68, NAT_1:13;
then i -' 1 in dom Fx by A40, A20, A10, FINSEQ_3:25;
hence (<*(a |^ n)*> ^ Fx) . i = ((n choose (2 * (i -' 1))) * (a |^ (n -' (2 * (i -' 1))))) * (((a ^2) -' 1) |^ (i -' 1)) by A41, A25, FINSEQ_3:103; :: thesis: verum

end;

suppose i <= 1 ; :: thesis: (<*(a |^ n)*> ^ Fx) . i = ((n choose (2 * (i -' 1))) * (a |^ (n -' (2 * (i -' 1))))) * (((a ^2) -' 1) |^ (i -' 1))

then A42: i = 1 by A24, XXREAL_0:1;
A43: n choose (2 * (i -' 1)) = 1 by A42, A25, NEWTON:19;
n -' (2 * (i -' 1)) = n - 0 by A42, A25, XREAL_1:233;
hence (<*(a |^ n)*> ^ Fx) . i = ((n choose (2 * (i -' 1))) * (a |^ (n -' (2 * (i -' 1))))) * (((a ^2) -' 1) |^ (i -' 1)) by A43, NEWTON:4, A42, A25; :: thesis: verum

end;

end;

end;

thus FY . i = (FxA . i) + (aFy . i) by RVSUM_1:11
.= (((n choose (2 * (i -' 1))) + (n choose ((2 * (i -' 1)) + 1))) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A38, A34, A37, A32, A25
.= (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A26, A25, NEWTON:22 ; :: thesis: verum

end;

Sum FX = (Sum AFx0) + (Sum AFy) by RVSUM_1:89
.= (Sum (a * Fx)) + (Sum (((a ^2) -' 1) * Fy)) by RVSUM_1:87, A15, A16 ;
hence (a |^ (n + 1)) + (Sum FX) = Px (a,(n + 1)) by A12, A13; :: thesis: ( len FX = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
len (AFx0 + AFy) = k + 1 by CARD_1:def 7;
hence len FX = [\((n + 1) / 2)/] by A19; :: thesis: for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i)
thus for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) :: thesis: verum

proof

let i be Nat; :: thesis: ( 1 <= i & i <= (n + 1) / 2 implies FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) )
assume A44: ( 1 <= i & i <= (n + 1) / 2 ) ; :: thesis: FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i)
set i1 = i -' 1;
(i -' 1) + 1 = i by A44, XREAL_1:235;
then A45: ((a ^2) -' 1) * (((a ^2) -' 1) |^ (i -' 1)) = ((a ^2) -' 1) |^ i by NEWTON:6;
Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A9, A44;
then A46: (((a ^2) -' 1) * Fy) . i = ((a ^2) -' 1) * (((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))) by VALUED_1:6
.= ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) by A45 ;
2 * i <= n + 1 by A44, XREAL_1:83;
then A47: (n + 1) -' (2 * i) = (n + 1) - (2 * i) by XREAL_1:233;
A48: (a * (Fx ^ <*0*>)) . i = a * ((Fx ^ <*0*>) . i) by VALUED_1:6;
A49: (a * (Fx ^ <*0*>)) . i = ((n choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i)

proof

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

suppose A50: i <= k ; :: thesis: (a * (Fx ^ <*0*>)) . i = ((n choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i)

then A51: 2 * i < n by A19, NAT_1:13, XREAL_1:66;
then i <= n / 2 by XREAL_1:77;
then A52: Fx . i = ((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2) -' 1) |^ i) by A11, A44;
A53: i in dom Fx by A44, A50, A10, A20, FINSEQ_3:25;
A54: n -' (2 * i) = n - (2 * i) by A51, XREAL_1:233;
(n + 1) -' (2 * i) = 1 + (n -' (2 * i)) by A54, A47;
then A55: a |^ ((n + 1) -' (2 * i)) = a * (a |^ (n -' (2 * i))) by NEWTON:6;
(a * (Fx ^ <*0*>)) . i = a * (((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2) -' 1) |^ i)) by A48, A52, A53, FINSEQ_1:def 7
.= ((n choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) by A55 ;
hence (a * (Fx ^ <*0*>)) . i = ((n choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ; :: thesis: verum

end;

suppose i > k ; :: thesis: (a * (Fx ^ <*0*>)) . i = ((n choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i)

then i >= k + 1 by NAT_1:13;
then A56: 2 * i >= 2 * (k + 1) by XREAL_1:66;
then A57: 2 * i >= n + 1 by A19;
2 * i <= n + 1 by A44, XREAL_1:83;
then A58: 2 * i = 2 * (k + 1) by A56, A19, XXREAL_0:1;
2 * i > n by A57, NAT_1:13;
then n choose (2 * i) = 0 by NEWTON:def 3;
hence (a * (Fx ^ <*0*>)) . i = ((n choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) by A58, A10, A20, A48; :: thesis: verum

end;

end;

end;

A59: ((2 * i) -' 1) + 1 = 2 * i by XREAL_1:235, NAT_1:14, A44;
thus FX . i = (AFx0 . i) + (AFy . i) by RVSUM_1:11
.= (((n choose ((2 * i) -' 1)) + (n choose (2 * i))) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) by A46, A49
.= (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) by A59, NEWTON:22 ; :: thesis: verum

end;

end;

suppose n is even ; :: thesis: S₁[n + 1]

then consider k being Nat such that
A60: n = 2 * k by ABIAN:def 2;
set k1 = k + 1;
A61: ( [\((n + 1) / 2)/] = k & [\(n / 2)/] = k ) by A60, Lm1;
then A62: ( len (<*(a |^ n)*> ^ Fx) = k + 1 & len (Fy ^ <*0*>) = k + 1 & len (a * (Fy ^ <*0*>)) = len (Fy ^ <*0*>) ) by FINSEQ_2:16, FINSEQ_5:8, A8, A10, RVSUM_1:117;
( rng (<*(a |^ n)*> ^ Fx) c= REAL & rng (a * (Fy ^ <*0*>)) c= REAL ) ;
then ( <*(a |^ n)*> ^ Fx is FinSequence of REAL & a * (Fy ^ <*0*>) is FinSequence of REAL ) by FINSEQ_1:def 4;
then reconsider FxA = <*(a |^ n)*> ^ Fx, aFy0 = a * (Fy ^ <*0*>) as Element of (k + 1) -tuples_on REAL by A62, FINSEQ_2:92;
rng ((<*(a |^ n)*> ^ Fx) + (a * (Fy ^ <*0*>))) c= NAT by VALUED_0:def 6;
then reconsider FY = (<*(a |^ n)*> ^ Fx) + (a * (Fy ^ <*0*>)) as FinSequence of NAT by FINSEQ_1:def 4;
A63: ( len (a * Fx) = len Fx & len Fx = k & len (((a ^2) -' 1) * Fy) = k ) by A61, A8, A10, RVSUM_1:117;
reconsider AFx = a * Fx, AFy = ((a ^2) -' 1) * Fy as Element of k -tuples_on REAL by A63, FINSEQ_2:92;
rng ((a * Fx) + (((a ^2) -' 1) * Fy)) c= NAT by VALUED_0:def 6;
then reconsider FX = (a * Fx) + (((a ^2) -' 1) * Fy) as FinSequence of NAT by FINSEQ_1:def 4;
take FY ; :: thesis: ex Fx being FinSequence of NAT st
( Sum FY = Py (a,(n + 1)) & len FY = [\(((n + 1) + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= ((n + 1) + 1) / 2 holds
FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ (n + 1)) + (Sum Fx) = Px (a,(n + 1)) & len Fx = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
Fx . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
take FX ; :: thesis: ( Sum FY = Py (a,(n + 1)) & len FY = [\(((n + 1) + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= ((n + 1) + 1) / 2 holds
FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ (n + 1)) + (Sum FX) = Px (a,(n + 1)) & len FX = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
thus Sum FY = (Sum FxA) + (Sum aFy0) by RVSUM_1:89
.= Py (a,(n + 1)) by A17, A14, RVSUM_1:87 ; :: thesis: ( len FY = [\(((n + 1) + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= ((n + 1) + 1) / 2 holds
FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ (n + 1)) + (Sum FX) = Px (a,(n + 1)) & len FX = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
len (FxA + aFy0) = k + 1 by CARD_1:def 7;
hence len FY = [\(((n + 1) + 1) / 2)/] by A60; :: thesis: ( ( for i being Nat st 1 <= i & i <= ((n + 1) + 1) / 2 holds
FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ (n + 1)) + (Sum FX) = Px (a,(n + 1)) & len FX = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
thus for i being Nat st 1 <= i & i <= ((n + 1) + 1) / 2 holds
FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) :: thesis: ( (a |^ (n + 1)) + (Sum FX) = Px (a,(n + 1)) & len FX = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )

proof

let i be Nat; :: thesis: ( 1 <= i & i <= ((n + 1) + 1) / 2 implies FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) )
assume A64: ( 1 <= i & i <= ((n + 1) + 1) / 2 ) ; :: thesis: FY . i = (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))
set i1 = i -' 1;
A65: (i -' 1) + 1 = i by A64, XREAL_1:235;
A66: 2 * i <= (n + 1) + 1 by A64, XREAL_1:83;
then A67: (2 * (i -' 1)) + 2 <= n + 2 by A65;
then A68: 2 * (i -' 1) <= n by XREAL_1:8;
A69: ( n -' (2 * (i -' 1)) = n - (2 * (i -' 1)) & ((n + 1) + 1) -' (2 * i) = ((n + 1) + 1) - (2 * i) ) by A67, A66, XREAL_1:8, XREAL_1:233;
2 * 1 <= 2 * i by A64, XREAL_1:66;
then A70: (2 * i) -' 1 = (2 * i) - 1 by XREAL_1:233, XXREAL_0:2;
A71: FxA . i = ((n choose (2 * (i -' 1))) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))

proof

per cases ( i > 1 or i <= 1 ) ;

suppose A72: i > 1 ; :: thesis: FxA . i = ((n choose (2 * (i -' 1))) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))

then A73: i -' 1 >= 1 by A65, NAT_1:13;
i -' 1 <= n / 2 by A68, XREAL_1:77;
then A74: Fx . (i -' 1) = ((n choose (2 * (i -' 1))) * (a |^ (n -' (2 * (i -' 1))))) * (((a ^2) -' 1) |^ (i -' 1)) by A11, A72, A65, NAT_1:13;
i -' 1 <= k by A68, A60, XREAL_1:68;
then i -' 1 in dom Fx by A73, A61, A10, FINSEQ_3:25;
hence FxA . i = ((n choose (2 * (i -' 1))) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A69, A74, A65, FINSEQ_3:103; :: thesis: verum

end;

suppose i <= 1 ; :: thesis: FxA . i = ((n choose (2 * (i -' 1))) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))

then A75: i = 1 by A64, XXREAL_0:1;
A76: n choose (2 * (i -' 1)) = 1 by A75, A65, NEWTON:19;
((n + 1) + 1) -' (2 * i) = (n + 2) - (2 * 1) by A75, NAT_1:11, XREAL_1:233;
hence FxA . i = ((n choose (2 * (i -' 1))) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A76, NEWTON:4, A75, A65; :: thesis: verum

end;

end;

end;

A77: (a * (Fy ^ <*0*>)) . i = ((n choose ((2 * (i -' 1)) + 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))

proof

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

suppose A78: i <= k ; :: thesis: (a * (Fy ^ <*0*>)) . i = ((n choose ((2 * (i -' 1)) + 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))

then A79: 2 * i <= n + 1 by NAT_1:13, A60, XREAL_1:66;
then A80: 2 * i <= (n + 1) + 1 by NAT_1:13;
i <= (n + 1) / 2 by A79, XREAL_1:77;
then A81: Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A9, A64;
i in dom Fy by A64, A78, A8, A61, FINSEQ_3:25;
then A82: Fy . i = (Fy ^ <*0*>) . i by FINSEQ_1:def 7;
A83: ( (n + 1) -' (2 * i) = (n + 1) - (2 * i) & ((n + 1) + 1) -' (2 * i) = ((n + 1) + 1) - (2 * i) ) by A79, A80, XREAL_1:233;
((n + 1) + 1) -' (2 * i) = 1 + ((n + 1) -' (2 * i)) by A83;
then A84: a |^ (((n + 1) + 1) -' (2 * i)) = a * (a |^ ((n + 1) -' (2 * i))) by NEWTON:6;
(a * (Fy ^ <*0*>)) . i = a * (((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))) by A81, A82, VALUED_1:6
.= ((n choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A84 ;
hence (a * (Fy ^ <*0*>)) . i = ((n choose ((2 * (i -' 1)) + 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A70, A65; :: thesis: verum

end;

suppose A85: i > k ; :: thesis: (a * (Fy ^ <*0*>)) . i = ((n choose ((2 * (i -' 1)) + 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))

then i -' 1 >= k by A65, NAT_1:13;
then A86: (2 * (i -' 1)) + 1 > n by NAT_1:13, A60, XREAL_1:66;
i >= k + 1 by A85, NAT_1:13;
then 2 * i >= 2 * (k + 1) by XREAL_1:66;
then 2 * i = 2 * (k + 1) by A60, A66, XXREAL_0:1;
then (Fy ^ <*0*>) . i = 0 by A8, A61;
then A87: (a * (Fy ^ <*0*>)) . i = a * 0 by VALUED_1:6;
n choose ((2 * (i -' 1)) + 1) = 0 by A86, NEWTON:def 3;
hence (a * (Fy ^ <*0*>)) . i = ((n choose ((2 * (i -' 1)) + 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A87; :: thesis: verum

end;

end;

end;

thus FY . i = (FxA . i) + (aFy0 . i) by RVSUM_1:11
.= (((n choose (2 * (i -' 1))) + (n choose ((2 * (i -' 1)) + 1))) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A71, A77
.= (((n + 1) choose ((2 * i) -' 1)) * (a |^ (((n + 1) + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A70, A65, NEWTON:22 ; :: thesis: verum

end;

Sum FX = (Sum AFx) + (Sum AFy) by RVSUM_1:89
.= (Sum (a * Fx)) + (Sum (((a ^2) -' 1) * Fy)) ;
hence (a |^ (n + 1)) + (Sum FX) = Px (a,(n + 1)) by A12, A13; :: thesis: ( len FX = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )
len (AFx + AFy) = k by CARD_1:def 7;
hence len FX = [\((n + 1) / 2)/] by A60, Lm1; :: thesis: for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i)
thus for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) :: thesis: verum

proof

let i be Nat; :: thesis: ( 1 <= i & i <= (n + 1) / 2 implies FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) )
assume A88: ( 1 <= i & i <= (n + 1) / 2 ) ; :: thesis: FX . i = (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i)
set i1 = i -' 1;
(i -' 1) + 1 = i by A88, XREAL_1:235;
then A89: ((a ^2) -' 1) * (((a ^2) -' 1) |^ (i -' 1)) = ((a ^2) -' 1) |^ i by NEWTON:6;
Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A9, A88;
then A90: (((a ^2) -' 1) * Fy) . i = ((a ^2) -' 1) * (((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1))) by VALUED_1:6
.= ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) by A89 ;
A91: 2 * i <= n + 1 by A88, XREAL_1:83;
then A92: (n + 1) -' (2 * i) = (n + 1) - (2 * i) by XREAL_1:233;
A93: 2 * i < n + 1 by A91, A60, XXREAL_0:1;
then A94: 2 * i <= n by NAT_1:13;
A95: i <= n / 2 by A93, NAT_1:13, XREAL_1:77;
A96: n -' (2 * i) = n - (2 * i) by A94, XREAL_1:233;
(n + 1) -' (2 * i) = 1 + (n -' (2 * i)) by A96, A92;
then A97: a |^ ((n + 1) -' (2 * i)) = a * (a |^ (n -' (2 * i))) by NEWTON:6;
A98: (a * Fx) . i = a * (Fx . i) by VALUED_1:6
.= a * (((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2) -' 1) |^ i)) by A95, A11, A88
.= ((n choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) by A97 ;
A99: ((2 * i) -' 1) + 1 = 2 * i by XREAL_1:235, NAT_1:14, A88;
thus FX . i = (AFx . i) + (AFy . i) by RVSUM_1:11
.= (((n choose ((2 * i) -' 1)) + (n choose (2 * i))) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) by A90, A98
.= (((n + 1) choose (2 * i)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ i) by A99, NEWTON:22 ; :: thesis: verum

end;

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A7);
hence ex Fy, Fx being FinSequence of NAT st
( Sum Fy = Py (a,n) & len Fy = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ n) + (Sum Fx) = Px (a,n) & len Fx = [\(n / 2)/] & ( for i being Nat st 1 <= i & i <= n / 2 holds
Fx . i = ((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) ) ; :: thesis: verum