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