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