let a be Nat; :: 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 S1[ Nat] means Product (f |^ $1) = (Product f) |^ $1;
A1: for b being Nat st S1[b] holds
S1[b + 1]
proof
let b be Nat; :: thesis: ( S1[b] implies S1[b + 1] )
assume A2: S1[b] ; :: thesis: S1[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: S1[ 0 ] ;
for b being Nat holds S1[b] from NAT_1:sch 2(A3, A1);
 hence Product (f |^ a) = (Product f) |^ a ; :: thesis: verum