let n be Nat; :: thesis: for a being Real holds Product ((a,a) Subnomial n) = a |^ (n * (n + 1))
let a be Real; :: thesis: Product ((a,a) Subnomial n) = a |^ (n * (n + 1))
set f = (n + 1) |-> (a |^ n);
set h = the_value_of ((n + 1) |-> (a |^ n));
set i = len ((n + 1) |-> (a |^ n));
Product ((a,a) Subnomial n) = Product ((n + 1) |-> (a |^ n)) by CONST1
.= (the_value_of ((n + 1) |-> (a |^ n))) |^ (len ((n + 1) |-> (a |^ n))) by RVSUM_3:8
.= a |^ (n * (n + 1)) by NEWTON:9 ;
hence Product ((a,a) Subnomial n) = a |^ (n * (n + 1)) ; :: thesis: verum