let a be natural number ; :: thesis: for f being FinSequence of REAL holds Product (f |^ a) = (Product f) |^ a
let f be FinSequence of REAL ; :: thesis: Product (f |^ a) = (Product f) |^ a
defpred S₁[ natural number ] means Product (f |^ $1) = (Product f) |^ $1;
A1: for b being natural number st S₁[b] holds
S₁[b + 1]

proof

let b be natural number ; :: thesis: ( S₁[b] implies S₁[b + 1] )
assume A2: S₁[b] ; :: thesis: S₁[b + 1]
thus Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f) by Th14
.= (Product f) |^ (b + 1) by A2, NEWTON:6 ; :: thesis: verum

end;

Product (f |^ 0) = Product ((len f) |-> 1) by Th9
.= 1 by RVSUM_1:102
.= (Product f) |^ 0 by NEWTON:4 ;
then A3: S₁[ 0 ] ;
for b being natural number holds S₁[b] from NAT_1:sch 2(A3, A1);
hence Product (f |^ a) = (Product f) |^ a ; :: thesis: verum