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