let b be natural number ; :: 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 S₁[ FinSequence of REAL ] means for b being natural number holds Product ($1 |^ (b + 1)) = (Product ($1 |^ b)) * (Product $1);

A1: now

let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of REAL ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A2: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
thus S₁[p ^ <*x*>] :: thesis: verum

proof

set p1 = p ^ <*x*>;
let b be natural number ; :: thesis: Product ((p ^ <*x*>) |^ (b + 1)) = (Product ((p ^ <*x*>) |^ b)) * (Product (p ^ <*x*>))
(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:127
.= ((Product (p |^ b)) * (Product p)) * (Product (<*x*> |^ (b + 1))) by A2
.= ((Product (p |^ b)) * (Product p)) * (Product <*(x |^ (b + 1))*>) by Th12
.= ((Product (p |^ b)) * (Product p)) * (x |^ (b + 1)) by RVSUM_1:125
.= ((Product (p |^ b)) * (Product p)) * ((x |^ b) * x) by NEWTON:11
.= (((Product (p |^ b)) * (x |^ b)) * x) * (Product p)
.= ((Product ((p |^ b) ^ <*(x |^ b)*>)) * x) * (Product p) by RVSUM_1:126
.= ((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:126 ;
:: thesis: verum

end;

end;

A3: S₁[ <*> REAL ]

proof

set f = <*> REAL ;
let b be natural number ; :: thesis: Product ((<*> REAL ) |^ (b + 1)) = (Product ((<*> REAL ) |^ b)) * (Product (<*> REAL ))
thus Product ((<*> REAL ) |^ (b + 1)) = 1 by Th11, RVSUM_1:124
.= (Product ((<*> REAL ) |^ b)) * (Product (<*> REAL )) by Th11, RVSUM_1:124 ; :: thesis: verum

end;

for p being FinSequence of REAL holds S₁[p] from FINSEQ_2:sch 2(A3, A1);
hence Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f) ; :: thesis: verum