let n be non zero Nat; :: thesis: 'I' . ((2 * n) + 1) = (Product (even-seq n)) / (Product (odd-seq (n + 1)))
defpred S₁[ non zero Nat] means 'I' . ((2 * $1) + 1) = (Product (even-seq $1)) / (Product (odd-seq ($1 + 1)));
A1: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
set Podd1 = Product (odd-seq (n + 1));
set Peven1 = Product (even-seq n);
A3: 2 < ((2 * n) + 1) + 2 by XREAL_1:29;
A4: ((2 * (n + 1)) + 1) * (Product (odd-seq (n + 1))) = Product (odd-seq ((n + 1) + 1)) by Th10;
'I' . ((2 * (n + 1)) + 1) = ((((2 * (n + 1)) + 1) -' 1) / ((2 * (n + 1)) + 1)) * ('I' . (((2 * (n + 1)) + 1) -' 2)) by Th36, A3
.= ((2 * (n + 1)) * (Product (even-seq n))) / (((2 * (n + 1)) + 1) * (Product (odd-seq (n + 1)))) by A2, A3, XCMPLX_1:76
.= (Product (even-seq (n + 1))) / (Product (odd-seq ((n + 1) + 1))) by Th9, A4 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A5: S₁[1]

proof

set n = 1;
A6: 3 -' 2 = 3 - 2 by XREAL_1:233
.= 1 ;
3 -' 1 = 3 - 1 by XREAL_1:233
.= 2 ;
then A8: 'I' . ((2 * 1) + 1) = (2 / 3) * ('I' . 1) by A6, Th36
.= (2 / 3) * 1 by Th33, Def6
.= 2 / 3 ;
(Product (even-seq 1)) / (Product (odd-seq (1 + 1))) = 2 / (1 * 3) by Th5, Th8, RVSUM_1:99
.= 2 / 3 ;
hence S₁[1] by A8; :: thesis: verum

end;

for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A5, A1);
hence 'I' . ((2 * n) + 1) = (Product (even-seq n)) / (Product (odd-seq (n + 1))) ; :: thesis: verum