let n be non zero Nat; :: thesis: Product (odd-seq (n + 1)) = ((2 * n) + 1) * (Product (odd-seq n))
Product (odd-seq (n + 1)) = Product ((odd-seq n) ^ <*((2 * n) + 1)*>) by Th7
.= (Product (odd-seq n)) * ((2 * n) + 1) by RVSUM_1:96 ;
hence Product (odd-seq (n + 1)) = ((2 * n) + 1) * (Product (odd-seq n)) ; :: thesis: verum