:: SERIES_4 semantic presentation

begin

      Lm1:  for a, b being real number holds
( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) )
proof
let a, b be real number ; ::_thesis: ( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) )
A1: (a + b) |^ (1 + 1) = ((a + b) |^ 1) * (a + b) by NEWTON:6
.= (a + b) * (a + b) by NEWTON:5
.= ((a * a) + (a * b)) + ((a * b) + (b * b))
.= ((a * a) + (a * b)) + ((a * b) + (b |^ 2)) by WSIERP_1:1
.= ((a |^ 2) + (a * b)) + ((a * b) + (b |^ 2)) by WSIERP_1:1
.= ((a |^ 2) + (2 * (a * b))) + (b |^ 2) ;
2 |^ 2 = 2 * 2 by WSIERP_1:1
.= 4 ;
hence  ( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) ) by A1; ::_thesis: verum
end;

Lm2:  for n being Element of NAT holds (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2 = (((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2
proof
let n be Element of NAT ; ::_thesis: (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2 = (((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2
(((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ (1 + 1) = ((((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 1) * (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) by NEWTON:6
.= (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) * (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) by NEWTON:5
.= ((((1 / 2) |^ (n + 1)) * ((1 / 2) |^ (n + 1))) + (((1 / 2) |^ (n + 1)) * (2 |^ (n + 1)))) + (((2 |^ (n + 1)) * ((1 / 2) |^ (n + 1))) + ((2 |^ (n + 1)) * (2 |^ (n + 1))))
.= ((((1 / 2) * (1 / 2)) |^ (n + 1)) + (((1 / 2) |^ (n + 1)) * (2 |^ (n + 1)))) + (((2 |^ (n + 1)) * ((1 / 2) |^ (n + 1))) + ((2 |^ (n + 1)) * (2 |^ (n + 1)))) by NEWTON:7
.= (((((1 / 2) * 1) / 2) |^ (n + 1)) + (((1 / 2) * 2) |^ (n + 1))) + (((2 |^ (n + 1)) * ((1 / 2) |^ (n + 1))) + ((2 |^ (n + 1)) * (2 |^ (n + 1)))) by NEWTON:7
.= (((((1 / 2) * 1) / 2) |^ (n + 1)) + (((1 / 2) * 2) |^ (n + 1))) + (((2 * (1 / 2)) |^ (n + 1)) + ((2 |^ (n + 1)) * (2 |^ (n + 1)))) by NEWTON:7
.= (((((1 / 2) * 1) / 2) |^ (n + 1)) + (((1 / 2) * 2) |^ (n + 1))) + (((2 * (1 / 2)) |^ (n + 1)) + ((2 * 2) |^ (n + 1))) by NEWTON:7
.= (((1 / 4) |^ (n + 1)) + 1) + ((1 |^ (n + 1)) + (4 |^ (n + 1))) by NEWTON:10
.= (((1 / 4) |^ (n + 1)) + 1) + (1 + (4 |^ (n + 1))) by NEWTON:10
.= (((1 / 4) |^ (n + 1)) + 2) + (4 |^ (n + 1)) ;
hence  (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2 = (((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2 ; ::_thesis: verum
end;

Lm3:  for n being Element of NAT holds (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2 = (((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2
proof
let n be Element of NAT ; ::_thesis: (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2 = (((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2
(((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ (1 + 1) = ((((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 1) * (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) by NEWTON:6
.= (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) * (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) by NEWTON:5
.= ((((1 / 3) |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + (((1 / 3) |^ (n + 1)) * (3 |^ (n + 1)))) + (((3 |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + ((3 |^ (n + 1)) * (3 |^ (n + 1))))
.= ((((1 / 3) * (1 / 3)) |^ (n + 1)) + (((1 / 3) |^ (n + 1)) * (3 |^ (n + 1)))) + (((3 |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + ((3 |^ (n + 1)) * (3 |^ (n + 1)))) by NEWTON:7
.= (((((1 / 3) * 1) / 3) |^ (n + 1)) + (((1 / 3) * 3) |^ (n + 1))) + (((3 |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + ((3 |^ (n + 1)) * (3 |^ (n + 1)))) by NEWTON:7
.= (((((1 / 3) * 1) / 3) |^ (n + 1)) + (((1 / 3) * 3) |^ (n + 1))) + (((3 * (1 / 3)) |^ (n + 1)) + ((3 |^ (n + 1)) * (3 |^ (n + 1)))) by NEWTON:7
.= (((((1 / 3) * 1) / 3) |^ (n + 1)) + (((1 / 3) * 3) |^ (n + 1))) + (((3 * (1 / 3)) |^ (n + 1)) + ((3 * 3) |^ (n + 1))) by NEWTON:7
.= (((1 / 9) |^ (n + 1)) + 1) + ((1 |^ (n + 1)) + (9 |^ (n + 1))) by NEWTON:10
.= (((1 / 9) |^ (n + 1)) + 1) + (1 + (9 |^ (n + 1))) by NEWTON:10
.= (((1 / 9) |^ (n + 1)) + 2) + (9 |^ (n + 1)) ;
hence  (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2 = (((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2 ; ::_thesis: verum
end;

Lm4:  for a, b being real number holds (a - b) * (a + b) = (a |^ 2) - (b |^ 2)
proof
let a, b be real number ; ::_thesis: (a - b) * (a + b) = (a |^ 2) - (b |^ 2)
(a - b) * (a + b) = (a * a) - (b * b)
.= (a |^ 2) - (b * b) by WSIERP_1:1
.= (a |^ 2) - (b |^ 2) by WSIERP_1:1 ;
hence  (a - b) * (a + b) = (a |^ 2) - (b |^ 2) ; ::_thesis: verum
end;

Lm5:  for a, b being real number holds (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2)
proof
let a, b be real number ; ::_thesis: (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2)
(a - b) |^ (1 + 1) = ((a - b) |^ 1) * (a - b) by NEWTON:6
.= (a - b) * (a - b) by NEWTON:5
.= ((a * a) - (a * b)) - ((a * b) - (b * b))
.= ((a * a) - (a * b)) - ((a * b) - (b |^ 2)) by WSIERP_1:1
.= ((a |^ 2) - (a * b)) - ((a * b) - (b |^ 2)) by WSIERP_1:1
.= ((a |^ 2) - (2 * (a * b))) + (b |^ 2) ;
hence  (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2) ; ::_thesis: verum
end;

Lm6:  for n being Element of NAT
for a being real number st a <> 1 holds
((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a))
proof
let n be Element of NAT ; ::_thesis: for a being real number st a <> 1 holds
((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a))
let a be real number ; ::_thesis: ( a <> 1 implies ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)) )
assume  a <> 1 ; ::_thesis: ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a))
then A1: 1 - a <> 0 ;
then ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - (((1 - a) * (n * (a |^ (n + 1)))) / ((1 - a) * (1 - a)))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) by XCMPLX_1:91
.= ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - (((1 - a) * (n * (a |^ (n + 1)))) / ((1 - a) |^ 2))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) by WSIERP_1:1
.= ((((a - (a * (a |^ n))) - ((n * (a |^ (n + 1))) - ((n * (a |^ (n + 1))) * a))) / ((1 - a) |^ 2)) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) by XCMPLX_1:120
.= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * 1)
.= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - a) / (1 - a)) * 1)) by A1, XCMPLX_1:60
.= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - a) / (1 - a)) * ((1 - a) / (1 - a)))) by A1, XCMPLX_1:60
.= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - a) * (1 - a)) / ((1 - a) * (1 - a)))) by XCMPLX_1:76
.= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * ((((1 - a) |^ 1) * (1 - a)) / ((1 - a) * (1 - a)))) by NEWTON:5
.= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - a) |^ (1 + 1)) / ((1 - a) * (1 - a)))) by NEWTON:6
.= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * ((((1 |^ 2) - ((2 * 1) * a)) + (a |^ 2)) / ((1 - a) * (1 - a)))) by Lm5
.= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * ((((1 |^ 2) - ((2 * 1) * a)) + (a |^ 2)) / ((1 - a) |^ 2))) by WSIERP_1:1
.= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - (2 * a)) + (a |^ 2)) / ((1 - a) |^ 2))) by NEWTON:10
.= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + ((((n * (a |^ (n + 1))) + (a |^ (n + 1))) * ((1 - (2 * a)) + (a |^ 2))) / ((1 - a) |^ 2)) by XCMPLX_1:74
.= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) + (((((n * (a |^ (n + 1))) * 1) - (((n * (a |^ (n + 1))) * 2) * a)) + ((n * (a |^ (n + 1))) * (a |^ 2))) + ((((a |^ (n + 1)) * 1) - (((a |^ (n + 1)) * 2) * a)) + ((a |^ (n + 1)) * (a |^ 2))))) / ((1 - a) |^ 2) by XCMPLX_1:62
.= ((((a - (a |^ (n + 1))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) + ((((n * (a |^ (n + 1))) - (((n * (a |^ (n + 1))) * 2) * a)) + ((n * (a |^ (n + 1))) * (a |^ 2))) + (((a |^ (n + 1)) - (((a |^ (n + 1)) * 2) * a)) + ((a |^ (n + 1)) * (a |^ 2))))) / ((1 - a) |^ 2) by NEWTON:6
.= ((a - ((a |^ (n + 1)) * a)) - (((n + 1) * (a |^ (n + 1))) * (a - (a |^ 2)))) / ((1 - a) |^ 2)
.= ((a - ((a |^ (n + 1)) * a)) - (((n + 1) * (a |^ (n + 1))) * (a - (a * a)))) / ((1 - a) |^ 2) by WSIERP_1:1
.= ((a - ((a |^ (n + 1)) * a)) / ((1 - a) |^ 2)) - (((((n + 1) * (a |^ (n + 1))) * a) * (1 - a)) / ((1 - a) |^ 2)) by XCMPLX_1:120
.= ((a - ((a |^ (n + 1)) * a)) / ((1 - a) |^ 2)) - (((((n + 1) * (a |^ (n + 1))) * a) * (1 - a)) / ((1 - a) * (1 - a))) by WSIERP_1:1
.= ((a - ((a |^ (n + 1)) * a)) / ((1 - a) |^ 2)) - ((((((n + 1) * (a |^ (n + 1))) * a) / (1 - a)) * (1 - a)) / (1 - a)) by XCMPLX_1:83
.= ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * ((a |^ (n + 1)) * a)) / (1 - a)) by A1, XCMPLX_1:87
.= ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ ((n + 1) + 1))) / (1 - a)) by NEWTON:6
.= ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)) ;
hence  ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)) ; ::_thesis: verum
end;

Lm7:  for n being Element of NAT holds 1 / ((2 -Root (n + 2)) + (2 -Root (n + 1))) = (2 -Root (n + 2)) - (2 -Root (n + 1))
proof
let n be Element of NAT ; ::_thesis: 1 / ((2 -Root (n + 2)) + (2 -Root (n + 1))) = (2 -Root (n + 2)) - (2 -Root (n + 1))
 (n + 1) + 1 > n + 1 by NAT_1:13;
then  2 -Root (n + 2) > 2 -Root (n + 1) by PREPOWER:28;
then  (2 -Root (n + 2)) - (2 -Root (n + 1)) > (2 -Root (n + 1)) - (2 -Root (n + 1)) by XREAL_1:9;
then (1 / ((2 -Root (n + 2)) + (2 -Root (n + 1)))) * 1 = (1 * ((2 -Root (n + 2)) - (2 -Root (n + 1)))) / (((2 -Root (n + 2)) - (2 -Root (n + 1))) * ((2 -Root (n + 2)) + (2 -Root (n + 1)))) by XCMPLX_1:91
.= ((2 -Root (n + 2)) - (2 -Root (n + 1))) / (((2 -Root (n + 2)) |^ 2) - ((2 -Root (n + 1)) |^ 2)) by Lm4
.= ((2 -Root (n + 2)) - (2 -Root (n + 1))) / ((n + 2) - ((2 -Root (n + 1)) |^ 2)) by PREPOWER:19
.= ((2 -Root (n + 2)) - (2 -Root (n + 1))) / ((n + 2) - (n + 1)) by PREPOWER:19
.= (2 -Root (n + 2)) - (2 -Root (n + 1)) ;
hence  1 / ((2 -Root (n + 2)) + (2 -Root (n + 1))) = (2 -Root (n + 2)) - (2 -Root (n + 1)) ; ::_thesis: verum
end;

theorem Th1: :: SERIES_4:1
for a, b, c being real number holds ((a + b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)
proof
let a, b, c be real number ; ::_thesis: ((a + b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)
((a + b) + c) |^ (1 + 1) = (((a + b) + c) |^ 1) * ((a + b) + c) by NEWTON:6
.= ((a + b) + c) * ((a + b) + c) by NEWTON:5
.= ((((a * a) + (a * b)) + (a * c)) + (((a * b) + (b * b)) + (b * c))) + (((a * c) + (c * b)) + (c * c))
.= ((((a * a) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c * c)) by WSIERP_1:1
.= ((((a |^ 2) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c * c)) by WSIERP_1:1
.= ((((a |^ 2) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c |^ 2)) by WSIERP_1:1
.= (((((a |^ 2) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)) + (b |^ 2) ;
hence  ((a + b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c) ; ::_thesis: verum
end;

theorem Th2: :: SERIES_4:2
for a, b being real number holds (a + b) |^ 3 = (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3)
proof
let a, b be real number ; ::_thesis: (a + b) |^ 3 = (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3)
(a + b) |^ (2 + 1) = ((a + b) |^ 2) * (a + b) by NEWTON:6
.= (((a |^ 2) + ((2 * a) * b)) + (b |^ 2)) * (a + b) by Lm1
.= ((((a |^ 2) * a) + ((a |^ 2) * b)) + ((((2 * a) * b) * a) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + ((b |^ 2) * b))
.= ((((a |^ 2) * a) + ((a |^ 2) * b)) + ((((2 * a) * b) * a) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ (2 + 1))) by NEWTON:6
.= (((a |^ 3) + ((a |^ 2) * b)) + (((2 * (a * a)) * b) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ 3)) by NEWTON:6
.= (((a |^ 3) + ((a |^ 2) * b)) + (((2 * ((a |^ 1) * a)) * b) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ 3)) by NEWTON:5
.= (((a |^ 3) + ((a |^ 2) * b)) + (((2 * (a |^ (1 + 1))) * b) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ 3)) by NEWTON:6
.= (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((2 * (b * b)) * a)) + (((b |^ 2) * a) + (b |^ 3))
.= (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((2 * ((b |^ 1) * b)) * a)) + (((b |^ 2) * a) + (b |^ 3)) by NEWTON:5
.= (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((2 * (b |^ (1 + 1))) * a)) + (((b |^ 2) * a) + (b |^ 3)) by NEWTON:6
.= (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3) ;
hence  (a + b) |^ 3 = (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3) ; ::_thesis: verum
end;

theorem :: SERIES_4:3
for a, b, c being real number holds ((a - b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c)
proof
let a, b, c be real number ; ::_thesis: ((a - b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c)
((a - b) + c) |^ (1 + 1) = (((a - b) + c) |^ 1) * ((a - b) + c) by NEWTON:6
.= ((a - b) + c) * ((a - b) + c) by NEWTON:5
.= ((((a * a) - (a * b)) + (a * c)) - (((a * b) - (b * b)) + (b * c))) + (((a * c) - (c * b)) + (c * c))
.= ((((a * a) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c * c)) by WSIERP_1:1
.= ((((a |^ 2) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c * c)) by WSIERP_1:1
.= ((((a |^ 2) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c |^ 2)) by WSIERP_1:1
.= (((((a |^ 2) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c)) + (b |^ 2) ;
hence  ((a - b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c) ; ::_thesis: verum
end;

theorem :: SERIES_4:4
for a, b, c being real number holds ((a - b) - c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c)
proof
let a, b, c be real number ; ::_thesis: ((a - b) - c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c)
((a - b) - c) |^ (1 + 1) = (((a - b) - c) |^ 1) * ((a - b) - c) by NEWTON:6
.= ((a - b) - c) * ((a - b) - c) by NEWTON:5
.= ((((a * a) - (a * b)) - (a * c)) - (((a * b) - (b * b)) - (b * c))) - (((a * c) - (c * b)) - (c * c))
.= ((((a * a) - (a * b)) - (a * c)) - (((a * b) - (b |^ 2)) - (b * c))) - (((a * c) - (c * b)) - (c * c)) by WSIERP_1:1
.= ((((a |^ 2) - (a * b)) - (a * c)) - (((a * b) - (b |^ 2)) - (b * c))) - (((a * c) - (c * b)) - (c * c)) by WSIERP_1:1
.= ((((a |^ 2) - (a * b)) - (a * c)) - (((a * b) - (b |^ 2)) - (b * c))) - (((a * c) - (c * b)) - (c |^ 2)) by WSIERP_1:1
.= (((((a |^ 2) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c)) + (b |^ 2) ;
hence  ((a - b) - c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c) ; ::_thesis: verum
end;

theorem :: SERIES_4:5
for a, b being real number holds (a - b) |^ 3 = (((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3)
proof
let a, b be real number ; ::_thesis: (a - b) |^ 3 = (((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3)
(a - b) |^ (2 + 1) = ((a - b) |^ 2) * (a - b) by NEWTON:6
.= (((a |^ 2) - ((2 * a) * b)) + (b |^ 2)) * (a - b) by Lm5
.= ((((a |^ 2) * a) - ((a |^ 2) * b)) - ((((2 * a) * b) * a) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - ((b |^ 2) * b))
.= ((((a |^ 2) * a) - ((a |^ 2) * b)) - ((((2 * a) * b) * a) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ (2 + 1))) by NEWTON:6
.= (((a |^ 3) - ((a |^ 2) * b)) - (((2 * (a * a)) * b) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ 3)) by NEWTON:6
.= (((a |^ 3) - ((a |^ 2) * b)) - (((2 * ((a |^ 1) * a)) * b) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ 3)) by NEWTON:5
.= (((a |^ 3) - ((a |^ 2) * b)) - (((2 * (a |^ (1 + 1))) * b) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ 3)) by NEWTON:6
.= ((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((2 * (b * b)) * a)) + ((b |^ 2) * a)) - (b |^ 3)
.= ((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((2 * ((b |^ 1) * b)) * a)) + ((b |^ 2) * a)) - (b |^ 3) by NEWTON:5
.= ((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((2 * (b |^ (1 + 1))) * a)) + ((b |^ 2) * a)) - (b |^ 3) by NEWTON:6
.= (((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3) ;
hence  (a - b) |^ 3 = (((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3) ; ::_thesis: verum
end;

theorem :: SERIES_4:6
for a, b being real number holds (a + b) |^ 4 = ((((a |^ 4) + ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) + ((4 * (b |^ 3)) * a)) + (b |^ 4)
proof
let a, b be real number ; ::_thesis: (a + b) |^ 4 = ((((a |^ 4) + ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) + ((4 * (b |^ 3)) * a)) + (b |^ 4)
(a + b) |^ (3 + 1) = ((a + b) |^ 3) * (a + b) by NEWTON:6
.= ((((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3)) * (a + b) by Th2
.= (((((a |^ 3) * a) + ((a |^ 3) * b)) + ((((3 * (a |^ 2)) * b) * a) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + ((b |^ 3) * b))
.= (((((a |^ 3) * a) + ((a |^ 3) * b)) + ((((3 * (a |^ 2)) * b) * a) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ (3 + 1))) by NEWTON:6
.= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * ((a |^ 2) * a)) * b) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:6
.= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ (2 + 1))) * b) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:6
.= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b * b)))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4))
.= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * ((b |^ 1) * b)))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:5
.= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ (1 + 1))))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:6
.= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a * a)) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4))
.= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * ((a |^ 1) * a)) + (((3 * (b |^ 2)) * b) * a))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:5
.= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a |^ (1 + 1))) + ((3 * ((b |^ 2) * b)) * a))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:6
.= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a |^ 2)) + ((3 * (b |^ (2 + 1))) * a))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:6
.= ((((a |^ 4) + ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) + ((4 * (b |^ 3)) * a)) + (b |^ 4) ;
hence  (a + b) |^ 4 = ((((a |^ 4) + ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) + ((4 * (b |^ 3)) * a)) + (b |^ 4) ; ::_thesis: verum
end;

theorem :: SERIES_4:7
for a, b, c, d being real number holds (((a + b) + c) + d) |^ 2 = ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d)
proof
let a, b, c, d be real number ; ::_thesis: (((a + b) + c) + d) |^ 2 = ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d)
(((a + b) + c) + d) |^ (1 + 1) = ((((a + b) + c) + d) |^ 1) * (((a + b) + c) + d) by NEWTON:6
.= (((a + b) + c) + d) * (((a + b) + c) + d) by NEWTON:5
.= ((((((a * a) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b * b)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c * c)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d))
.= ((((((a * a) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c * c)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d)) by WSIERP_1:1
.= ((((((a |^ 2) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c * c)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d)) by WSIERP_1:1
.= ((((((a |^ 2) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c |^ 2)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d)) by WSIERP_1:1
.= ((((((a |^ 2) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c |^ 2)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d |^ 2)) by WSIERP_1:1
.= ((((((a |^ 2) + (c |^ 2)) + (b |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d) ;
hence  (((a + b) + c) + d) |^ 2 = ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d) ; ::_thesis: verum
end;

theorem :: SERIES_4:8
for a, b, c being real number holds ((a + b) + c) |^ 3 = ((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c)
proof
let a, b, c be real number ; ::_thesis: ((a + b) + c) |^ 3 = ((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c)
((a + b) + c) |^ (2 + 1) = (((a + b) + c) |^ 2) * ((a + b) + c) by NEWTON:6
.= ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)) * ((a + b) + c) by Th1
.= ((((((((a |^ 2) * a) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + ((b |^ 2) * b)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + ((c |^ 2) * c))) + (((((2 * a) * b) * a) + (((2 * a) * b) * b)) + (((2 * a) * b) * c))) + (((((2 * a) * c) * a) + (((2 * a) * c) * b)) + (((2 * a) * c) * c))) + (((((2 * b) * c) * a) + (((2 * b) * c) * b)) + (((2 * b) * c) * c))
.= (((((((a |^ (2 + 1)) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + ((b |^ 2) * b)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + ((c |^ 2) * c))) + (((((2 * a) * b) * a) + (((2 * a) * b) * b)) + (((2 * a) * b) * c))) + (((((2 * a) * c) * a) + (((2 * a) * c) * b)) + (((2 * a) * c) * c))) + (((((2 * b) * c) * a) + (((2 * b) * c) * b)) + (((2 * b) * c) * c)) by NEWTON:6
.= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ (2 + 1))) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + ((c |^ 2) * c))) + (((((2 * a) * b) * a) + (((2 * a) * b) * b)) + (((2 * a) * b) * c))) + (((((2 * a) * c) * a) + (((2 * a) * c) * b)) + (((2 * a) * c) * c))) + (((((2 * b) * c) * a) + (((2 * b) * c) * b)) + (((2 * b) * c) * c)) by NEWTON:6
.= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a * a)) * b) + ((2 * a) * (b * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by NEWTON:6
.= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * ((a |^ 1) * a)) * b) + ((2 * a) * (b * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by NEWTON:5
.= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ (1 + 1))) * b) + ((2 * a) * (b * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by NEWTON:6
.= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * ((b |^ 1) * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by NEWTON:5
.= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ (1 + 1)))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by NEWTON:6
.= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by WSIERP_1:1
.= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c |^ 2)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by WSIERP_1:1
.= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c |^ 2)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c |^ 2))) by WSIERP_1:1
.= (((((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + (((b |^ 2) * a) + ((b |^ 2) * c))) + (((c |^ 2) * a) + ((c |^ 2) * b))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c |^ 2)))) + (((((2 * b) * c) * a) + ((2 * (b |^ 2)) * c)) + ((2 * (c |^ 2)) * b)) by WSIERP_1:1
.= ((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c) ;
hence  ((a + b) + c) |^ 3 = ((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c) ; ::_thesis: verum
end;

theorem :: SERIES_4:9
for n being Element of NAT
for a being real number st a <> 0 holds
(((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2
proof
let n be Element of NAT ; ::_thesis: for a being real number st a <> 0 holds
(((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2
let a be real number ; ::_thesis: ( a <> 0 implies (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2 )
assume A1: a <> 0 ; ::_thesis: (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2
(((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ (1 + 1) = ((((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 1) * (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) by NEWTON:6
.= (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) * (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) by NEWTON:5
.= ((((1 / a) |^ (n + 1)) * ((1 / a) |^ (n + 1))) + (((1 / a) |^ (n + 1)) * (a |^ (n + 1)))) + (((a |^ (n + 1)) * ((1 / a) |^ (n + 1))) + ((a |^ (n + 1)) * (a |^ (n + 1))))
.= ((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) |^ (n + 1)) * (a |^ (n + 1)))) + (((a |^ (n + 1)) * ((1 / a) |^ (n + 1))) + ((a |^ (n + 1)) * (a |^ (n + 1)))) by NEWTON:7
.= ((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) * a) |^ (n + 1))) + (((a |^ (n + 1)) * ((1 / a) |^ (n + 1))) + ((a |^ (n + 1)) * (a |^ (n + 1)))) by NEWTON:7
.= ((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) * a) |^ (n + 1))) + (((a * (1 / a)) |^ (n + 1)) + ((a |^ (n + 1)) * (a |^ (n + 1)))) by NEWTON:7
.= ((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) * a) |^ (n + 1))) + (((a * (1 / a)) |^ (n + 1)) + ((a * a) |^ (n + 1))) by NEWTON:7
.= ((((1 / a) * (1 / a)) |^ (n + 1)) + (1 |^ (n + 1))) + ((((1 / a) * a) |^ (n + 1)) + ((a * a) |^ (n + 1))) by A1, XCMPLX_1:106
.= ((((1 / a) * (1 / a)) |^ (n + 1)) + (1 |^ (n + 1))) + ((1 |^ (n + 1)) + ((a * a) |^ (n + 1))) by A1, XCMPLX_1:106
.= ((((1 / a) * (1 / a)) |^ (n + 1)) + 1) + ((1 |^ (n + 1)) + ((a * a) |^ (n + 1))) by NEWTON:10
.= ((((1 / a) * (1 / a)) |^ (n + 1)) + 1) + (1 + ((a * a) |^ (n + 1))) by NEWTON:10
.= ((((1 / a) * (1 / a)) |^ (n + 1)) + ((a * a) |^ (n + 1))) + 2
.= ((((1 / a) * (1 / a)) |^ (n + 1)) + ((a |^ 2) |^ (n + 1))) + 2 by WSIERP_1:1
.= ((((1 / a) * (1 / a)) |^ (n + 1)) + (a |^ (2 * (n + 1)))) + 2 by NEWTON:9
.= ((((1 / a) |^ 2) |^ (n + 1)) + (a |^ ((2 * n) + 2))) + 2 by WSIERP_1:1
.= (((1 / a) |^ (2 * (n + 1))) + (a |^ ((2 * n) + 2))) + 2 by NEWTON:9
.= (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2 ;
hence  (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2 ; ::_thesis: verum
end;

theorem :: SERIES_4:10
for n being Element of NAT
for a being real number
for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . n = a |^ n ) holds
(Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a)
proof
let n be Element of NAT ; ::_thesis: for a being real number
for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . n = a |^ n ) holds
(Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a)
let a be real number ; ::_thesis: for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . n = a |^ n ) holds
(Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a)
let s be Real_Sequence; ::_thesis: ( a <> 1 & ( for n being Element of NAT holds s . n = a |^ n ) implies (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) )
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = (1 - (a |^ ($1 + 1))) / (1 - a);
assume  a <> 1 ; ::_thesis: ( ex n being Element of NAT st not s . n = a |^ n or (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) )
then A1: 1 - a <> 0 ;
assume A2: for n being Element of NAT holds s . n = a |^ n ; ::_thesis: (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a)
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ; ::_thesis: S1[n + 1]
hence (Partial_Sums s) . (n + 1) = ((1 - (a |^ (n + 1))) / (1 - a)) + (s . (n + 1)) by SERIES_1:def_1
.= ((1 - (a |^ (n + 1))) / (1 - a)) + ((a |^ (n + 1)) * 1) by A2
.= ((1 - (a |^ (n + 1))) / (1 - a)) + ((a |^ (n + 1)) * ((1 - a) / (1 - a))) by A1, XCMPLX_1:60
.= ((1 - (a |^ (n + 1))) / (1 - a)) + (((a |^ (n + 1)) * (1 - a)) / (1 - a)) by XCMPLX_1:74
.= ((1 - (a |^ (n + 1))) + ((a |^ (n + 1)) - ((a |^ (n + 1)) * a))) / (1 - a) by XCMPLX_1:62
.= ((1 - (a |^ (n + 1))) + ((a |^ (n + 1)) - (a |^ ((n + 1) + 1)))) / (1 - a) by NEWTON:6
.= (1 - (a |^ ((n + 1) + 1))) / (1 - a) ;
::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= a |^ 0 by A2
.= 1 by NEWTON:4
.= (1 - a) / (1 - a) by A1, XCMPLX_1:60
.= (1 - (a |^ (0 + 1))) / (1 - a) by NEWTON:5 ;
then A4: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3);
hence  (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ; ::_thesis: verum
end;

theorem :: SERIES_4:11
for a being real number
for s being Real_Sequence st a <> 1 & a <> 0 & ( for n being Element of NAT holds s . n = (1 / a) |^ n ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a)
proof
let a be real number ; ::_thesis: for s being Real_Sequence st a <> 1 & a <> 0 & ( for n being Element of NAT holds s . n = (1 / a) |^ n ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a)
let s be Real_Sequence; ::_thesis: ( a <> 1 & a <> 0 & ( for n being Element of NAT holds s . n = (1 / a) |^ n ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) )
assume that
A1: a <> 1 and
A2: a <> 0 ; ::_thesis: ( ex n being Element of NAT st not s . n = (1 / a) |^ n or for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) )
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = (((1 / a) |^ $1) - a) / (1 - a);
assume A3: for n being Element of NAT holds s . n = (1 / a) |^ n ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a)
A4: 1 - a <> 0 by A1;
A5: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) ; ::_thesis: S1[n + 1]
hence (Partial_Sums s) . (n + 1) = ((((1 / a) |^ n) - a) / (1 - a)) + (s . (n + 1)) by SERIES_1:def_1
.= ((((1 / a) |^ n) - a) / (1 - a)) + (((1 / a) |^ (n + 1)) * 1) by A3
.= ((((1 / a) |^ n) - a) / (1 - a)) + (((1 / a) |^ (n + 1)) * ((1 - a) / (1 - a))) by A4, XCMPLX_1:60
.= ((((1 / a) |^ n) - a) / (1 - a)) + ((((1 / a) |^ (n + 1)) * (1 - a)) / (1 - a)) by XCMPLX_1:74
.= ((((1 / a) |^ n) - a) + ((((1 / a) |^ (n + 1)) * 1) - (((1 / a) |^ (n + 1)) * a))) / (1 - a) by XCMPLX_1:62
.= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - (((1 / a) |^ (n + 1)) * a)) / (1 - a)
.= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - ((((1 / a) |^ n) * (1 / a)) * a)) / (1 - a) by NEWTON:6
.= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - (((1 / a) |^ n) * ((1 / a) * a))) / (1 - a)
.= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - (((1 / a) |^ n) * 1)) / (1 - a) by A2, XCMPLX_1:106
.= (((1 / a) |^ (n + 1)) - a) / (1 - a) ;
::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= (1 / a) |^ 0 by A3
.= 1 by NEWTON:4
.= (1 - a) / (1 - a) by A4, XCMPLX_1:60
.= (((1 / a) |^ 0) - a) / (1 - a) by NEWTON:4 ;
then A6: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A5);
hence  for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) ; ::_thesis: verum
end;

theorem :: SERIES_4:12
for n being Element of NAT
for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((10 |^ n) + (2 * n)) + 1 ) holds
(Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2)
proof
let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((10 |^ n) + (2 * n)) + 1 ) holds
(Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2)
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((10 |^ n) + (2 * n)) + 1 ) implies (Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2) )
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = (((10 |^ ($1 + 1)) / 9) - (1 / 9)) + (($1 + 1) |^ 2);
assume A1: for n being Element of NAT holds s . n = ((10 |^ n) + (2 * n)) + 1 ; ::_thesis: (Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2)
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2) ; ::_thesis: S1[n + 1]
then (Partial_Sums s) . (n + 1) = ((((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2)) + (s . (n + 1)) by SERIES_1:def_1
.= ((((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2)) + (((10 |^ (n + 1)) + (2 * (n + 1))) + 1) by A1
.= ((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + ((((n + 1) |^ 2) + (2 * n)) + 3)
.= ((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + (((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) + (2 * n)) + 3) by Lm1
.= ((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + (((((n |^ 2) + (2 * n)) + 1) + (2 * n)) + 3) by NEWTON:10
.= ((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + (((n |^ 2) + ((2 * n) * 2)) + (2 |^ 2)) by Lm1
.= ((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + ((n + 2) |^ 2) by Lm1
.= (((10 |^ ((n + 1) + 1)) / 9) - (1 / 9)) + ((n + 2) |^ 2) by NEWTON:6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= ((10 |^ 0) + (2 * 0)) + 1 by A1
.= ((10 / 9) - (1 / 9)) + 1 by NEWTON:4
.= (((10 |^ (0 + 1)) / 9) - (1 / 9)) + 1 by NEWTON:5
.= (((10 |^ (0 + 1)) / 9) - (1 / 9)) + ((0 + 1) |^ 2) by NEWTON:10 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  (Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2) ; ::_thesis: verum
end;

theorem :: SERIES_4:13
for n being Element of NAT
for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) - 1) + ((1 / 2) |^ n) ) holds
(Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n)
proof
let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) - 1) + ((1 / 2) |^ n) ) holds
(Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n)
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((2 * n) - 1) + ((1 / 2) |^ n) ) implies (Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n) )
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = (($1 |^ 2) + 1) - ((1 / 2) |^ $1);
assume A1: for n being Element of NAT holds s . n = ((2 * n) - 1) + ((1 / 2) |^ n) ; ::_thesis: (Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n)
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n) ; ::_thesis: S1[n + 1]
then (Partial_Sums s) . (n + 1) = (((n |^ 2) + 1) - ((1 / 2) |^ n)) + (s . (n + 1)) by SERIES_1:def_1
.= (((n |^ 2) + 1) - ((1 / 2) |^ n)) + (((2 * (n + 1)) - 1) + ((1 / 2) |^ (n + 1))) by A1
.= (((((n |^ 2) + 1) - ((1 / 2) |^ n)) + ((1 / 2) |^ (n + 1))) + (2 * (n + 1))) - 1
.= (((((n |^ 2) + 1) - ((1 / 2) |^ n)) + (((1 / 2) |^ n) * (1 / 2))) + (2 * (n + 1))) - 1 by NEWTON:6
.= ((((n |^ 2) + 1) - (((1 / 2) |^ n) * (1 / 2))) + (2 * (n + 1))) - 1
.= ((((n |^ 2) + 1) - ((1 / 2) |^ (n + 1))) + (2 * (n + 1))) - 1 by NEWTON:6
.= ((((n |^ 2) + (2 * n)) + 1) + 1) - ((1 / 2) |^ (n + 1))
.= ((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) + 1) - ((1 / 2) |^ (n + 1)) by NEWTON:10
.= (((n + 1) |^ 2) + 1) - ((1 / 2) |^ (n + 1)) by Lm1 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= ((2 * 0) - 1) + ((1 / 2) |^ 0) by A1
.= (- 1) + 1 by NEWTON:4
.= (1 - 1) + (0 |^ 2) by NEWTON:11
.= (1 - ((1 / 2) |^ 0)) + (0 |^ 2) by NEWTON:4 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  (Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n) ; ::_thesis: verum
end;

theorem :: SERIES_4:14
for n being Element of NAT
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n * ((1 / 2) |^ n) ) holds
(Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n))
proof
let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = n * ((1 / 2) |^ n) ) holds
(Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n))
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n * ((1 / 2) |^ n) ) implies (Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n)) )
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = 2 - ((2 + $1) * ((1 / 2) |^ $1));
assume A1: for n being Element of NAT holds s . n = n * ((1 / 2) |^ n) ; ::_thesis: (Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n))
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n)) ; ::_thesis: S1[n + 1]
then (Partial_Sums s) . (n + 1) = (2 - ((2 + n) * ((1 / 2) |^ n))) + (s . (n + 1)) by SERIES_1:def_1
.= (2 - ((2 + n) * ((1 / 2) |^ n))) + ((n + 1) * ((1 / 2) |^ (n + 1))) by A1
.= (((2 - (2 * ((1 / 2) |^ n))) - (n * ((1 / 2) |^ n))) + (n * ((1 / 2) |^ (n + 1)))) + (1 * ((1 / 2) |^ (n + 1)))
.= (((2 - (((4 * 1) / 2) * ((1 / 2) |^ n))) - (n * ((1 / 2) |^ n))) + (n * (((1 / 2) |^ n) * (1 / 2)))) + (1 * ((1 / 2) |^ (n + 1))) by NEWTON:6
.= (((2 - (4 * (((1 / 2) |^ n) * (1 / 2)))) - (n * ((1 / 2) |^ n))) + ((n * ((1 / 2) |^ n)) * (1 / 2))) + (1 * ((1 / 2) |^ (n + 1)))
.= (((2 - (4 * ((1 / 2) |^ (n + 1)))) - (n * ((1 / 2) |^ n))) + ((n * ((1 / 2) |^ n)) * (1 / 2))) + (1 * ((1 / 2) |^ (n + 1))) by NEWTON:6
.= (2 - (3 * ((1 / 2) |^ (n + 1)))) - (n * (((1 / 2) |^ n) * (1 / 2)))
.= (2 - (3 * ((1 / 2) |^ (n + 1)))) - (n * ((1 / 2) |^ (n + 1))) by NEWTON:6
.= 2 - ((3 + n) * ((1 / 2) |^ (n + 1))) ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= 0 * ((1 / 2) |^ 0) by A1
.= 2 - ((2 + 0) * 1)
.= 2 - ((2 + 0) * ((1 / 2) |^ 0)) by NEWTON:4 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  (Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n)) ; ::_thesis: verum
end;

theorem :: SERIES_4:15
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (((1 / 2) |^ n) + (2 |^ n)) |^ 2 ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (((1 / 2) |^ n) + (2 |^ n)) |^ 2 ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3 )
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = (((- (((1 / 4) |^ $1) / 3)) + ((4 |^ ($1 + 1)) / 3)) + (2 * $1)) + 3;
assume A1: for n being Element of NAT holds s . n = (((1 / 2) |^ n) + (2 |^ n)) |^ 2 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = (((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3 ; ::_thesis: S1[n + 1]
then (Partial_Sums s) . (n + 1) = ((((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3) + (s . (n + 1)) by SERIES_1:def_1
.= ((((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3) + ((((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2) by A1
.= ((((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3) + ((((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2) by Lm2
.= (((((- (((1 / 4) |^ n) / 3)) + ((1 / 4) |^ (n + 1))) + ((4 |^ (n + 1)) / 3)) + (4 |^ (n + 1))) + (2 * (n + 1))) + 3
.= (((((- (((1 / 4) |^ n) / 3)) + (((1 / 4) |^ n) * (1 / 4))) + ((4 |^ (n + 1)) / 3)) + (4 |^ (n + 1))) + (2 * (n + 1))) + 3 by NEWTON:6
.= ((((- ((((1 / 4) |^ n) * (1 / 4)) / 3)) + ((4 |^ (n + 1)) / 3)) + (4 |^ (n + 1))) + (2 * (n + 1))) + 3
.= ((((- (((1 / 4) |^ (n + 1)) / 3)) + ((4 |^ (n + 1)) / 3)) + (4 |^ (n + 1))) + (2 * (n + 1))) + 3 by NEWTON:6
.= (((- (((1 / 4) |^ (n + 1)) / 3)) + (((4 |^ (n + 1)) * 4) / 3)) + (2 * (n + 1))) + 3
.= (((- (((1 / 4) |^ (n + 1)) / 3)) + ((4 |^ ((n + 1) + 1)) / 3)) + (2 * (n + 1))) + 3 by NEWTON:6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= (((1 / 2) |^ 0) + (2 |^ 0)) |^ 2 by A1
.= (1 + (2 |^ 0)) |^ 2 by NEWTON:4
.= (1 + 1) |^ 2 by NEWTON:4
.= (((- (1 / 3)) + (4 / 3)) + (2 * 0)) + 3 by Lm1
.= (((- (((1 / 4) |^ 0) / 3)) + (4 / 3)) + (2 * 0)) + 3 by NEWTON:4
.= (((- (((1 / 4) |^ 0) / 3)) + ((4 |^ (0 + 1)) / 3)) + (2 * 0)) + 3 by NEWTON:5 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3 ; ::_thesis: verum
end;

theorem :: SERIES_4:16
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (((1 / 3) |^ n) + (3 |^ n)) |^ 2 ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (((1 / 3) |^ n) + (3 |^ n)) |^ 2 ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3 )
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = (((- (((1 / 9) |^ $1) / 8)) + ((9 |^ ($1 + 1)) / 8)) + (2 * $1)) + 3;
assume A1: for n being Element of NAT holds s . n = (((1 / 3) |^ n) + (3 |^ n)) |^ 2 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = (((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3 ; ::_thesis: S1[n + 1]
then (Partial_Sums s) . (n + 1) = ((((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3) + (s . (n + 1)) by SERIES_1:def_1
.= ((((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3) + ((((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2) by A1
.= ((((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3) + ((((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2) by Lm3
.= (((((- (((1 / 9) |^ n) / 8)) + ((1 / 9) |^ (n + 1))) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3
.= (((((- (((1 / 9) |^ n) / 8)) + (((1 / 9) |^ n) * (1 / 9))) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3 by NEWTON:6
.= ((((- ((((1 / 9) |^ n) * (1 / 9)) / 8)) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3
.= ((((- (((1 / 9) |^ (n + 1)) / 8)) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3 by NEWTON:6
.= (((- (((1 / 9) |^ (n + 1)) / 8)) + (((9 |^ (n + 1)) * 9) / 8)) + (2 * (n + 1))) + 3
.= (((- (((1 / 9) |^ (n + 1)) / 8)) + ((9 |^ ((n + 1) + 1)) / 8)) + (2 * (n + 1))) + 3 by NEWTON:6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= (((1 / 3) |^ 0) + (3 |^ 0)) |^ 2 by A1
.= (1 + (3 |^ 0)) |^ 2 by NEWTON:4
.= (1 + 1) |^ 2 by NEWTON:4
.= (((- (1 / 8)) + (9 / 8)) + (2 * 0)) + 3 by Lm1
.= (((- (((1 / 9) |^ 0) / 8)) + (9 / 8)) + (2 * 0)) + 3 by NEWTON:4
.= (((- (((1 / 9) |^ 0) / 8)) + ((9 |^ (0 + 1)) / 8)) + (2 * 0)) + 3 by NEWTON:5 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3 ; ::_thesis: verum
end;

theorem :: SERIES_4:17
for s being Real_Sequence st ( for n being Element of NAT holds s . n = n * (2 |^ n) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n * (2 |^ n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2 )
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = (($1 * (2 |^ ($1 + 1))) - (2 |^ ($1 + 1))) + 2;
assume A1: for n being Element of NAT holds s . n = n * (2 |^ n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = ((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2 ; ::_thesis: S1[n + 1]
then (Partial_Sums s) . (n + 1) = (((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2) + (s . (n + 1)) by SERIES_1:def_1
.= (((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2) + ((n + 1) * (2 |^ (n + 1))) by A1
.= (n * ((2 |^ (n + 1)) * 2)) + 2
.= (n * (2 |^ ((n + 1) + 1))) + 2 by NEWTON:6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= 0 * (2 |^ 0) by A1
.= ((0 * (2 |^ (0 + 1))) - 2) + 2
.= ((0 * (2 |^ (0 + 1))) - (2 |^ (0 + 1))) + 2 by NEWTON:5 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  for n being Element of NAT holds (Partial_Sums s) . n = ((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2 ; ::_thesis: verum
end;

theorem :: SERIES_4:18
for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) + 1) * (3 |^ n) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = (n * (3 |^ (n + 1))) + 1
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((2 * n) + 1) * (3 |^ n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = (n * (3 |^ (n + 1))) + 1 )
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = ($1 * (3 |^ ($1 + 1))) + 1;
assume A1: for n being Element of NAT holds s . n = ((2 * n) + 1) * (3 |^ n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (n * (3 |^ (n + 1))) + 1
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = (n * (3 |^ (n + 1))) + 1 ; ::_thesis: S1[n + 1]
then (Partial_Sums s) . (n + 1) = ((n * (3 |^ (n + 1))) + 1) + (s . (n + 1)) by SERIES_1:def_1
.= ((n * (3 |^ (n + 1))) + 1) + (((2 * (n + 1)) + 1) * (3 |^ (n + 1))) by A1
.= ((n + 1) * ((3 |^ (n + 1)) * 3)) + 1
.= ((n + 1) * (3 |^ ((n + 1) + 1))) + 1 by NEWTON:6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= ((2 * 0) + 1) * (3 |^ 0) by A1
.= (0 * (3 |^ (0 + 1))) + 1 by NEWTON:4 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  for n being Element of NAT holds (Partial_Sums s) . n = (n * (3 |^ (n + 1))) + 1 ; ::_thesis: verum
end;

theorem :: SERIES_4:19
for a being real number
for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . n = n * (a |^ n) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))
proof
let a be real number ; ::_thesis: for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . n = n * (a |^ n) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))
let s be Real_Sequence; ::_thesis: ( a <> 1 & ( for n being Element of NAT holds s . n = n * (a |^ n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a)) )
assume that
A1: a <> 1 and
A2: for n being Element of NAT holds s . n = n * (a |^ n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = ((a * (1 - (a |^ $1))) / ((1 - a) |^ 2)) - (($1 * (a |^ ($1 + 1))) / (1 - a));
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a)) ; ::_thesis: S1[n + 1]
then (Partial_Sums s) . (n + 1) = (((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (s . (n + 1)) by SERIES_1:def_1
.= (((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + ((n + 1) * (a |^ (n + 1))) by A2
.= ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1))
.= ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)) by A1, Lm6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= 0 * (a |^ 0) by A2
.= (((1 - 1) * a) / ((1 - a) |^ 2)) - ((0 * (a |^ (0 + 1))) / (1 - a))
.= (((1 - (a |^ 0)) * a) / ((1 - a) |^ 2)) - ((0 * (a |^ (0 + 1))) / (1 - a)) by NEWTON:4 ;
then A4: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3);
hence  for n being Element of NAT holds (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a)) ; ::_thesis: verum
end;

theorem :: SERIES_4:20
for n being Element of NAT
for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ) holds
(Partial_Sums s) . n = 2 -Root (n + 1)
proof
let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ) holds
(Partial_Sums s) . n = 2 -Root (n + 1)
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ) implies (Partial_Sums s) . n = 2 -Root (n + 1) )
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = 2 -Root ($1 + 1);
assume A1: for n being Element of NAT holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ; ::_thesis: (Partial_Sums s) . n = 2 -Root (n + 1)
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = 2 -Root (n + 1) ; ::_thesis: S1[n + 1]
then (Partial_Sums s) . (n + 1) = (2 -Root (n + 1)) + (s . (n + 1)) by SERIES_1:def_1
.= (2 -Root (n + 1)) + (1 / ((2 -Root ((n + 1) + 1)) + (2 -Root (n + 1)))) by A1
.= (2 -Root (n + 1)) + ((2 -Root (n + 2)) - (2 -Root (n + 1))) by Lm7
.= 2 -Root (n + 2) ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= 1 / ((2 -Root (0 + 1)) + (2 -Root 0)) by A1
.= 1 / ((2 -Root (0 + 1)) + 0) by PREPOWER:def_2
.= 1 / 1 by PREPOWER:20
.= 2 -Root (0 + 1) by PREPOWER:20 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  (Partial_Sums s) . n = 2 -Root (n + 1) ; ::_thesis: verum
end;

theorem :: SERIES_4:21
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (2 |^ n) + ((1 / 2) |^ n) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (2 |^ n) + ((1 / 2) |^ n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1 )
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = ((2 |^ ($1 + 1)) - ((1 / 2) |^ $1)) + 1;
assume A1: for n being Element of NAT holds s . n = (2 |^ n) + ((1 / 2) |^ n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Sums s) . n = ((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1 ; ::_thesis: S1[n + 1]
then (Partial_Sums s) . (n + 1) = (((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1) + (s . (n + 1)) by SERIES_1:def_1
.= (((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1) + ((2 |^ (n + 1)) + ((1 / 2) |^ (n + 1))) by A1
.= ((((- ((1 / 2) |^ n)) + 1) + ((1 / 2) |^ (n + 1))) + (2 |^ (n + 1))) + (2 |^ (n + 1))
.= ((((- ((1 / 2) |^ n)) + 1) + (((1 / 2) |^ n) * (1 / 2))) + (2 |^ (n + 1))) + (2 |^ (n + 1)) by NEWTON:6
.= (((- (((1 / 2) |^ n) * (1 / 2))) + 1) + (2 |^ (n + 1))) + (2 |^ (n + 1))
.= (((- ((1 / 2) |^ (n + 1))) + 1) + (2 |^ (n + 1))) + (2 |^ (n + 1)) by NEWTON:6
.= ((- ((1 / 2) |^ (n + 1))) + 1) + ((2 |^ (n + 1)) * 2)
.= ((- ((1 / 2) |^ (n + 1))) + 1) + (2 |^ ((n + 1) + 1)) by NEWTON:6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1
.= (2 |^ 0) + ((1 / 2) |^ 0) by A1
.= 1 + ((1 / 2) |^ 0) by NEWTON:4
.= (2 - 1) + 1 by NEWTON:4
.= ((2 |^ (0 + 1)) - 1) + 1 by NEWTON:5
.= ((2 |^ (0 + 1)) - ((1 / 2) |^ 0)) + 1 by NEWTON:4 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1 ; ::_thesis: verum
end;

theorem :: SERIES_4:22
for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((n !) * n) + (n / ((n + 1) !)) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = ((n + 1) !) - (1 / ((n + 1) !))
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((n !) * n) + (n / ((n + 1) !)) ) implies for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = ((n + 1) !) - (1 / ((n + 1) !)) )
defpred S1[ Nat] means (Partial_Sums s) . $1 = (($1 + 1) !) - (1 / (($1 + 1) !));
assume A1: for n being Element of NAT holds s . n = ((n !) * n) + (n / ((n + 1) !)) ; ::_thesis: for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = ((n + 1) !) - (1 / ((n + 1) !))
then A2: s . 0 = ((0 !) * 0) + (0 / ((0 + 1) !))
.= 0 ;
A3: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A4: (Partial_Sums s) . n = ((n + 1) !) - (1 / ((n + 1) !)) ; ::_thesis: S1[n + 1]
 n in NAT by ORDINAL1:def_12;
then (Partial_Sums s) . (n + 1) = (((n + 1) !) - (1 / ((n + 1) !))) + (s . (n + 1)) by A4, SERIES_1:def_1
.= (((n + 1) !) - (1 / ((n + 1) !))) + ((((n + 1) !) * (n + 1)) + ((n + 1) / (((n + 1) + 1) !))) by A1
.= ((((n + 1) !) + (((n + 1) !) * (n + 1))) - (1 / ((n + 1) !))) + ((n + 1) / (((n + 1) + 1) !))
.= ((((n + 1) !) * ((n + 1) + 1)) - ((1 * (n + 2)) / (((n + 1) !) * ((n + 1) + 1)))) + ((n + 1) / ((n + 2) !)) by XCMPLX_1:91
.= ((((n + 1) !) * ((n + 1) + 1)) - ((1 * (n + 2)) / (((n + 1) + 1) !))) + ((n + 1) / ((n + 2) !)) by NEWTON:15
.= (((n + 1) !) * ((n + 1) + 1)) - (((n + 2) / (((n + 1) + 1) !)) - ((n + 1) / ((n + 2) !)))
.= (((n + 1) !) * ((n + 1) + 1)) - (((n + 2) - (n + 1)) / ((n + 2) !)) by XCMPLX_1:120
.= (((n + 1) + 1) !) - (1 / (((n + 1) + 1) !)) by NEWTON:15 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . (1 + 0) = ((Partial_Sums s) . 0) + (s . (1 + 0)) by SERIES_1:def_1
.= 0 + (s . 1) by A2, SERIES_1:def_1
.= ((1 !) * 1) + (1 / ((1 + 1) !)) by A1
.= ((((1 + 1) !) - 1) + 1) - (1 / ((1 + 1) !)) by NEWTON:13, NEWTON:14 ;
then A5: S1[1] ;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A5, A3);
hence  for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = ((n + 1) !) - (1 / ((n + 1) !)) ; ::_thesis: verum
end;

theorem :: SERIES_4:23
for a being real number
for s being Real_Sequence st a <> 1 & ( for n being Element of NAT st n >= 1 holds
( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1)
proof
let a be real number ; ::_thesis: for s being Real_Sequence st a <> 1 & ( for n being Element of NAT st n >= 1 holds
( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1)
let s be Real_Sequence; ::_thesis: ( a <> 1 & ( for n being Element of NAT st n >= 1 holds
( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) )
defpred S1[ Nat] means (Partial_Sums s) . $1 = a * (((a / (a - 1)) |^ $1) - 1);
assume  a <> 1 ; ::_thesis: ( ex n being Element of NAT st
( n >= 1 & not ( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) or for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) )
then A1: a - 1 <> 0 ;
assume A2: for n being Element of NAT st n >= 1 holds
( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1)
A3: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A4: (Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) ; ::_thesis: S1[n + 1]
A5: n + 1 >= 1 by NAT_1:11;
 n in NAT by ORDINAL1:def_12;
then (Partial_Sums s) . (n + 1) = (a * (((a / (a - 1)) |^ n) - 1)) + (s . (n + 1)) by A4, SERIES_1:def_1
.= ((a * ((a / (a - 1)) |^ n)) - a) + ((a / (a - 1)) |^ (n + 1)) by A2, A5
.= ((a * ((a / (a - 1)) |^ n)) + ((a / (a - 1)) |^ (n + 1))) - a
.= ((a * ((a / (a - 1)) |^ n)) + (((a / (a - 1)) |^ n) * (a / (a - 1)))) - a by NEWTON:6
.= (((a / (a - 1)) |^ n) * ((a * 1) + (a / (a - 1)))) - a
.= (((a / (a - 1)) |^ n) * ((a * 1) + (a * (1 / (a - 1))))) - a by XCMPLX_1:99
.= (((a / (a - 1)) |^ n) * (a * (1 + (1 / (a - 1))))) - a
.= (((a / (a - 1)) |^ n) * (a * (((a - 1) / (a - 1)) + (1 / (a - 1))))) - a by A1, XCMPLX_1:60
.= (((a / (a - 1)) |^ n) * (a * (((a - 1) + 1) / (a - 1)))) - a by XCMPLX_1:62
.= (a * (((a / (a - 1)) |^ n) * (a / (a - 1)))) - a
.= (a * ((a / (a - 1)) |^ (n + 1))) - a by NEWTON:6
.= a * (((a / (a - 1)) |^ (n + 1)) - 1) ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . (0 + 1) = ((Partial_Sums s) . 0) + (s . (0 + 1)) by SERIES_1:def_1
.= (s . 0) + (s . 1) by SERIES_1:def_1
.= 0 + (s . 1) by A2
.= 0 + ((a / (a - 1)) |^ 1) by A2
.= ((a / (a - 1)) + a) - a by NEWTON:5
.= ((a * (1 / (a - 1))) + (a * 1)) - a by XCMPLX_1:99
.= ((a * (1 / (a - 1))) + (a * ((a - 1) / (a - 1)))) - a by A1, XCMPLX_1:60
.= (a * ((1 / (a - 1)) + ((a - 1) / (a - 1)))) - a
.= (a * ((1 + (a - 1)) / (a - 1))) - a by XCMPLX_1:62
.= a * ((a / (a - 1)) - 1)
.= a * (((a / (a - 1)) |^ 1) - 1) by NEWTON:5 ;
then A6: S1[1] ;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A6, A3);
hence  for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) ; ::_thesis: verum
end;

theorem :: SERIES_4:24
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = (2 |^ n) * (((3 * n) - 1) / 4) & s . 0 = 0 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = ((2 |^ n) * (((3 * n) - 4) / 2)) + 2
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds
( s . n = (2 |^ n) * (((3 * n) - 1) / 4) & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = ((2 |^ n) * (((3 * n) - 4) / 2)) + 2 )
defpred S1[ Nat] means (Partial_Sums s) . $1 = ((2 |^ $1) * (((3 * $1) - 4) / 2)) + 2;
assume A1: for n being Element of NAT st n >= 1 holds
( s . n = (2 |^ n) * (((3 * n) - 1) / 4) & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = ((2 |^ n) * (((3 * n) - 4) / 2)) + 2
A2: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A3: (Partial_Sums s) . n = ((2 |^ n) * (((3 * n) - 4) / 2)) + 2 ; ::_thesis: S1[n + 1]
A4: n + 1 >= 1 by NAT_1:11;
 n in NAT by ORDINAL1:def_12;
then (Partial_Sums s) . (n + 1) = (((2 |^ n) * (((3 * n) - 4) / 2)) + 2) + (s . (n + 1)) by A3, SERIES_1:def_1
.= (((2 |^ n) * (((3 * n) - 4) / 2)) + 2) + ((2 |^ (n + 1)) * (((3 * (n + 1)) - 1) / 4)) by A1, A4
.= (((2 |^ n) * (((3 * n) - 4) / 2)) + ((2 |^ (n + 1)) * (((3 * n) + 2) / 4))) + 2
.= (((2 |^ n) * (((3 * n) - 4) / 2)) + (((2 |^ n) * 2) * (((3 * n) + 2) / 4))) + 2 by NEWTON:6
.= (((2 |^ n) * 2) * (((3 * n) - 1) / 2)) + 2
.= ((2 |^ (n + 1)) * (((3 * (n + 1)) - 4) / 2)) + 2 by NEWTON:6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums s) . (1 + 0) = ((Partial_Sums s) . 0) + (s . (1 + 0)) by SERIES_1:def_1
.= (s . 0) + (s . 1) by SERIES_1:def_1
.= 0 + (s . 1) by A1
.= (2 |^ 1) * (((3 * 1) - 1) / 4) by A1
.= 2 * (1 / 2) by NEWTON:5
.= (((3 - 4) / 2) * 2) + 2
.= (((3 - 4) / 2) * (2 |^ 1)) + 2 by NEWTON:5
.= (((2 |^ 1) * ((3 * 1) - 4)) / 2) + 2 ;
then A5: S1[1] ;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A5, A2);
hence  for n being Element of NAT st n >= 1 holds
(Partial_Sums s) . n = ((2 |^ n) * (((3 * n) - 4) / 2)) + 2 ; ::_thesis: verum
end;

theorem :: SERIES_4:25
for n being Element of NAT
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n + 1) / (n + 2) ) holds
(Partial_Product s) . n = 1 / (n + 2)
proof
let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n + 1) / (n + 2) ) holds
(Partial_Product s) . n = 1 / (n + 2)
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (n + 1) / (n + 2) ) implies (Partial_Product s) . n = 1 / (n + 2) )
defpred S1[ Element of NAT ] means (Partial_Product s) . $1 = 1 / ($1 + 2);
assume A1: for n being Element of NAT holds s . n = (n + 1) / (n + 2) ; ::_thesis: (Partial_Product s) . n = 1 / (n + 2)
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Product s) . n = 1 / (n + 2) ; ::_thesis: S1[n + 1]
then (Partial_Product s) . (n + 1) = (1 / (n + 2)) * (s . (n + 1)) by SERIES_3:def_1
.= (1 / (n + 2)) * (((n + 1) + 1) / ((n + 1) + 2)) by A1
.= ((1 / (n + 2)) * (n + 2)) / ((n + 1) + 2) by XCMPLX_1:74
.= 1 / ((n + 1) + 2) by XCMPLX_1:106 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Product s) . 0 = s . 0 by SERIES_3:def_1
.= (0 + 1) / (0 + 2) by A1
.= 1 / (0 + 2) ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  (Partial_Product s) . n = 1 / (n + 2) ; ::_thesis: verum
end;

theorem :: SERIES_4:26
for n being Element of NAT
for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / (n + 1) ) holds
(Partial_Product s) . n = 1 / ((n + 1) !)
proof
let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / (n + 1) ) holds
(Partial_Product s) . n = 1 / ((n + 1) !)
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = 1 / (n + 1) ) implies (Partial_Product s) . n = 1 / ((n + 1) !) )
defpred S1[ Element of NAT ] means (Partial_Product s) . $1 = 1 / (($1 + 1) !);
assume A1: for n being Element of NAT holds s . n = 1 / (n + 1) ; ::_thesis: (Partial_Product s) . n = 1 / ((n + 1) !)
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  (Partial_Product s) . n = 1 / ((n + 1) !) ; ::_thesis: S1[n + 1]
then (Partial_Product s) . (n + 1) = (1 / ((n + 1) !)) * (s . (n + 1)) by SERIES_3:def_1
.= (1 / ((n + 1) !)) * (1 / ((n + 1) + 1)) by A1
.= ((1 / ((n + 1) !)) * 1) / ((n + 1) + 1) by XCMPLX_1:74
.= 1 / (((n + 1) !) * ((n + 1) + 1)) by XCMPLX_1:78
.= 1 / ((n + 2) !) by NEWTON:15 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Product s) . 0 = s . 0 by SERIES_3:def_1
.= 1 / ((0 + 1) !) by A1, NEWTON:13 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence  (Partial_Product s) . n = 1 / ((n + 1) !) ; ::_thesis: verum
end;

theorem :: SERIES_4:27
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = n & s . 0 = 1 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = n !
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds
( s . n = n & s . 0 = 1 ) ) implies for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = n ! )
defpred S1[ Nat] means (Partial_Product s) . $1 = $1 ! ;
assume A1: for n being Element of NAT st n >= 1 holds
( s . n = n & s . 0 = 1 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = n !
A2: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A3: (Partial_Product s) . n = n ! ; ::_thesis: S1[n + 1]
A4: n + 1 >= 1 by NAT_1:11;
 n in NAT by ORDINAL1:def_12;
then (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def_1
.= (n !) * (n + 1) by A1, A3, A4
.= (n + 1) ! by NEWTON:15 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Product s) . (1 + 0) = ((Partial_Product s) . 0) * (s . (1 + 0)) by SERIES_3:def_1
.= (s . 0) * (s . (1 + 0)) by SERIES_3:def_1
.= 1 * (s . 1) by A1
.= 1 ! by A1, NEWTON:13 ;
then A5: S1[1] ;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A5, A2);
hence  for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = n ! ; ::_thesis: verum
end;

theorem :: SERIES_4:28
for a being real number
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = a / n & s . 0 = 1 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = (a |^ n) / (n !)
proof
let a be real number ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = a / n & s . 0 = 1 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = (a |^ n) / (n !)
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds
( s . n = a / n & s . 0 = 1 ) ) implies for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = (a |^ n) / (n !) )
defpred S1[ Nat] means (Partial_Product s) . $1 = (a |^ $1) / ($1 !);
assume A1: for n being Element of NAT st n >= 1 holds
( s . n = a / n & s . 0 = 1 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = (a |^ n) / (n !)
A2: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A3: (Partial_Product s) . n = (a |^ n) / (n !) ; ::_thesis: S1[n + 1]
A4: n + 1 >= 1 by NAT_1:11;
 n in NAT by ORDINAL1:def_12;
then (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def_1
.= ((a |^ n) / (n !)) * (a / (n + 1)) by A1, A3, A4
.= ((a |^ n) * a) / ((n !) * (n + 1)) by XCMPLX_1:76
.= (a |^ (n + 1)) / ((n !) * (n + 1)) by NEWTON:6
.= (a |^ (n + 1)) / ((n + 1) !) by NEWTON:15 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Product s) . (1 + 0) = ((Partial_Product s) . 0) * (s . (1 + 0)) by SERIES_3:def_1
.= (s . 0) * (s . (1 + 0)) by SERIES_3:def_1
.= 1 * (s . 1) by A1
.= (1 * a) / 1 by A1
.= (a |^ 1) / (1 !) by NEWTON:5, NEWTON:13 ;
then A5: S1[1] ;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A5, A2);
hence  for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = (a |^ n) / (n !) ; ::_thesis: verum
end;

theorem :: SERIES_4:29
for a being real number
for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = a & s . 0 = 1 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = a |^ n
proof
let a be real number ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds
( s . n = a & s . 0 = 1 ) ) holds
for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = a |^ n
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds
( s . n = a & s . 0 = 1 ) ) implies for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = a |^ n )
defpred S1[ Nat] means (Partial_Product s) . $1 = a |^ $1;
assume A1: for n being Element of NAT st n >= 1 holds
( s . n = a & s . 0 = 1 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = a |^ n
A2: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A3: (Partial_Product s) . n = a |^ n ; ::_thesis: S1[n + 1]
A4: n + 1 >= 1 by NAT_1:11;
 n in NAT by ORDINAL1:def_12;
then (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def_1
.= (a |^ n) * a by A1, A3, A4
.= a |^ (n + 1) by NEWTON:6 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Product s) . (1 + 0) = ((Partial_Product s) . 0) * (s . (1 + 0)) by SERIES_3:def_1
.= (s . 0) * (s . (1 + 0)) by SERIES_3:def_1
.= 1 * (s . 1) by A1
.= 1 * a by A1
.= a |^ 1 by NEWTON:5 ;
then A5: S1[1] ;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A5, A2);
hence  for n being Element of NAT st n >= 1 holds
(Partial_Product s) . n = a |^ n ; ::_thesis: verum
end;

theorem :: SERIES_4:30
for s being Real_Sequence st ( for n being Element of NAT st n >= 2 holds
( s . n = 1 - (1 / (n |^ 2)) & s . 0 = 1 & s . 1 = 1 ) ) holds
for n being Element of NAT st n >= 2 holds
(Partial_Product s) . n = (n + 1) / (2 * n)
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 2 holds
( s . n = 1 - (1 / (n |^ 2)) & s . 0 = 1 & s . 1 = 1 ) ) implies for n being Element of NAT st n >= 2 holds
(Partial_Product s) . n = (n + 1) / (2 * n) )
defpred S1[ Nat] means (Partial_Product s) . $1 = ($1 + 1) / (2 * $1);
assume A1: for n being Element of NAT st n >= 2 holds
( s . n = 1 - (1 / (n |^ 2)) & s . 0 = 1 & s . 1 = 1 ) ; ::_thesis: for n being Element of NAT st n >= 2 holds
(Partial_Product s) . n = (n + 1) / (2 * n)
A2: for n being Nat st n >= 2 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 2 & S1[n] implies S1[n + 1] )
assume that
A3: n >= 2 and
A4: (Partial_Product s) . n = (n + 1) / (2 * n) ; ::_thesis: S1[n + 1]
A5: n + 1 > 1 + 1 by A3, NAT_1:13;
 (n + 1) * (n + 1) <> 0 ;
then A6: (n + 1) |^ 2 <> 0 by WSIERP_1:1;
 n in NAT by ORDINAL1:def_12;
then (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def_1
.= ((n + 1) / (2 * n)) * (1 - (1 / ((n + 1) |^ 2))) by A1, A4, A5
.= ((n + 1) / (2 * n)) * ((((n + 1) |^ 2) / ((n + 1) |^ 2)) - (1 / ((n + 1) |^ 2))) by A6, XCMPLX_1:60
.= ((n + 1) / (2 * n)) * ((((n + 1) |^ 2) - 1) / ((n + 1) |^ 2)) by XCMPLX_1:120
.= ((n + 1) / (2 * n)) * ((((n + 1) |^ 2) - (1 |^ 2)) / ((n + 1) |^ 2)) by NEWTON:10
.= ((n + 1) / (2 * n)) * ((((n + 1) - 1) * ((n + 1) + 1)) / ((n + 1) |^ 2)) by Lm4
.= ((n + 1) * (n * (n + 2))) / ((2 * n) * ((n + 1) |^ 2)) by XCMPLX_1:76
.= (((n + 1) * n) * (n + 2)) / ((2 * n) * ((n + 1) * (n + 1))) by WSIERP_1:1
.= (((n + 1) * n) * (n + 2)) / ((n * (n + 1)) * (2 * (n + 1)))
.= (((n + 1) * n) / (n * (n + 1))) * ((n + 2) / (2 * (n + 1))) by XCMPLX_1:76
.= (((n + 1) / (n + 1)) * (n / n)) * ((n + 2) / (2 * (n + 1))) by XCMPLX_1:76
.= (1 * (n / n)) * ((n + 2) / (2 * (n + 1))) by XCMPLX_1:60
.= (1 * 1) * ((n + 2) / (2 * (n + 1))) by A3, XCMPLX_1:60
.= (n + 2) / (2 * (n + 1)) ;
hence  S1[n + 1] ; ::_thesis: verum
end;
(Partial_Product s) . (1 + 1) = ((Partial_Product s) . (1 + 0)) * (s . 2) by SERIES_3:def_1
.= (((Partial_Product s) . 0) * (s . 1)) * (s . 2) by SERIES_3:def_1
.= ((s . 0) * (s . 1)) * (s . 2) by SERIES_3:def_1
.= (1 * (s . 1)) * (s . 2) by A1
.= (1 * 1) * (s . 2) by A1
.= 1 - (1 / 4) by A1, Lm1
.= (2 + 1) / (2 * 2) ;
then A7: S1[2] ;
 for n being Nat st n >= 2 holds
S1[n] from NAT_1:sch_8(A7, A2);
hence  for n being Element of NAT st n >= 2 holds
(Partial_Product s) . n = (n + 1) / (2 * n) ; ::_thesis: verum
end;