let k be non zero Nat; :: thesis: Product (even-seq k) = (2 |^ k) * (k !)
defpred S₁[ Nat] means Product (even-seq $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] )
A3: 2 |^ (n + 1) = (2 |^ 1) * (2 |^ n) by NEWTON:8
.= 2 * (2 |^ n) ;
assume S₁[n] ; :: thesis: S₁[n + 1]
then Product (even-seq (n + 1)) = (2 * (n + 1)) * ((2 |^ n) * (n !)) by Th9
.= (2 |^ (n + 1)) * ((n + 1) * (n !)) by A3
.= (2 |^ (n + 1)) * ((n + 1) !) by NEWTON:15 ;
hence S₁[n + 1] ; :: thesis: verum

end;

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