let b be Nat; :: thesis: for f being FinSequence of REAL holds Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f)
let f be FinSequence of REAL ; :: thesis: Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f)
defpred S1[ FinSequence of REAL ] means for b being Nat holds Product ($1 |^ (b + 1)) = (Product ($1 |^ b)) * (Product $1);
A1: now :: thesis: for p being FinSequence of REAL
for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]
let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]
let x be Element of REAL ; :: thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: S1[p] ; :: thesis: S1[p ^ <*x*>]
thus S1[p ^ <*x*>] :: thesis: verum
proof
set p1 = p ^ <*x*>;
let b be Nat; :: thesis: Product ((p ^ <*x*>) |^ (b + 1)) = (Product ((p ^ <*x*>) |^ b)) * (Product (p ^ <*x*>))
reconsider xb1 = x |^ (b + 1), xb = x |^ b as Real ;
(p ^ <*x*>) |^ (b + 1) = (p |^ (b + 1)) ^ (<*x*> |^ (b + 1)) by Th13;
hence Product ((p ^ <*x*>) |^ (b + 1)) = (Product (p |^ (b + 1))) * (Product (<*x*> |^ (b + 1))) by RVSUM_1:97
.= ((Product (p |^ b)) * (Product p)) * (Product (<*x*> |^ (b + 1))) by A2
.= ((Product (p |^ b)) * (Product p)) * (Product <*xb1*>) by Th12
.= ((Product (p |^ b)) * (Product p)) * (x |^ (b + 1))
.= ((Product (p |^ b)) * (Product p)) * ((x |^ b) * x) by NEWTON:6
.= (((Product (p |^ b)) * (x |^ b)) * x) * (Product p)
.= ((Product ((p |^ b) ^ <*xb*>)) * x) * (Product p) by RVSUM_1:96
.= ((Product ((p |^ b) ^ (<*x*> |^ b))) * x) * (Product p) by Th12
.= ((Product ((p ^ <*x*>) |^ b)) * x) * (Product p) by Th13
.= (Product ((p ^ <*x*>) |^ b)) * ((Product p) * x)
.= (Product ((p ^ <*x*>) |^ b)) * (Product (p ^ <*x*>)) by RVSUM_1:96 ;
:: thesis: verum
end;
end;
A3: S1[ <*> REAL]
proof
set f = <*> REAL;
let b be Nat; :: thesis: Product ((<*> REAL) |^ (b + 1)) = (Product ((<*> REAL) |^ b)) * (Product (<*> REAL))
thus Product ((<*> REAL) |^ (b + 1)) = 1 by Th11, RVSUM_1:94
.= (Product ((<*> REAL) |^ b)) * (Product (<*> REAL)) by Th11, RVSUM_1:94 ; :: thesis: verum
end;
for p being FinSequence of REAL holds S1[p] from FINSEQ_2:sch 2(A3, A1);
 hence Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f) ; :: thesis: verum