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 S₁[ 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 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 2 & S₁[n] implies S₁[n + 1] )
assume that
A3: n >= 2 and
A4: (Partial_Product s) . n = (n + 1) / (2 * n) ; :: thesis: S₁[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 S₁[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: S₁[2] ;
for n being Nat st n >= 2 holds
S₁[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