let a be Real; :: thesis: Mean <*a*> = a
len <*a*> = 1 by CARD_1:def 7;
hence Mean <*a*> = a ; :: thesis: verum