let a, b, c, d be Real; :: thesis: Mean <*a,b,c,d*> = (((a + b) + c) + d) / 4
len <*a,b,c,d*> = 4 by CARD_1:def 7;
hence Mean <*a,b,c,d*> = (((a + b) + c) + d) / 4 by Th20; :: thesis: verum