let a, b, c be positive Real; :: thesis: (GMean <*a,b,c*>) |^ 3 = (a * b) * c
set f = <*a,b,c*>;
A1: Product <*a,b,c*> = (a * b) * c by RVSUM_1:100;
len <*a,b,c*> = 3 by CARD_1:def 7;
hence (GMean <*a,b,c*>) |^ 3 = (a * b) * c by A1; :: thesis: verum