let n be Nat; :: thesis: for a being non negative Real holds Product ((a,1) Subnomial n) = a |^ ((n + 1) choose 2)
let a be non negative Real; :: thesis: Product ((a,1) Subnomial n) = a |^ ((n + 1) choose 2)
set l = a |^ (n choose 2);
set f = (a,1) Subnomial n;
set g = (1,a) Subnomial n;
A1: ((n + 1) choose 2) * 2 = ((n * (n + 1)) / 2) * 2 by NUMPOLY1:72
.= n * (n + 1) ;
A2: (a |^ ((n + 1) choose 2)) |^ 2 = a |^ (((n + 1) choose 2) * 2) by NEWTON:9
.= Product (((a * 1),(a * 1)) Subnomial n) by A1, PRA
.= Product (((a,1) Subnomial n) (#) ((1,a) Subnomial n)) by ST
.= (Product ((a,1) Subnomial n)) * (Product ((1,a) Subnomial n)) by PRN
.= (Product ((a,1) Subnomial n)) * (Product ((a,1) Subnomial n)) by SFE, RVSUM_3:4
.= (Product ((a,1) Subnomial n)) |^ 2 by NEWTON:81 ;
a |^ ((n + 1) choose 2) = sqrt ((Product ((a,1) Subnomial n)) |^ 2) by A2
.= Product ((a,1) Subnomial n) ;
hence Product ((a,1) Subnomial n) = a |^ ((n + 1) choose 2) ; :: thesis: verum