let k be non zero Nat; :: thesis: Product (odd-seq k) = ((2 * k) !) / ((2 |^ k) * (k !))
defpred S₁[ non zero Nat] means Product (odd-seq $1) = ((2 * $1) !) / ((2 |^ $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]
A3: ((2 * (n + 1)) * ((2 * n) + 1)) * ((2 * n) !) = (2 * (n + 1)) * (((2 * n) + 1) * ((2 * n) !))
.= (((2 * n) + 1) + 1) * (((2 * n) + 1) !) by NEWTON:15
.= (2 * (n + 1)) ! by NEWTON:15 ;
2 |^ (n + 1) = (2 |^ 1) * (2 |^ n) by NEWTON:8
.= 2 * (2 |^ n) ;
then A5: ((2 * (n + 1)) * (2 |^ n)) * (n !) = (2 |^ (n + 1)) * ((n + 1) * (n !))
.= (2 |^ (n + 1)) * ((n + 1) !) by NEWTON:15 ;
((2 * n) + 1) * (Product (odd-seq n)) = (((2 * (n + 1)) * ((2 * n) + 1)) / (2 * (n + 1))) * (((2 * n) !) / ((2 |^ n) * (n !))) by A2, XCMPLX_1:89
.= ((2 * (n + 1)) !) / ((2 * (n + 1)) * ((2 |^ n) * (n !))) by A3, XCMPLX_1:76
.= ((2 * (n + 1)) !) / ((2 |^ (n + 1)) * ((n + 1) !)) by A5 ;
hence S₁[n + 1] by Th10; :: thesis: verum

end;

A6: S₁[1] by Th8, NEWTON:14, NEWTON:13;
for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A6, A1);
hence Product (odd-seq k) = ((2 * k) !) / ((2 |^ k) * (k !)) ; :: thesis: verum