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