:: deftheorem defines are_gamma-equivalent RVSUM_3:def 6 :
for f1, f2 being real-valued FinSequence holds
( f1,f2 are_gamma-equivalent iff ( len f1 = len f2 & Mean f1 = Mean f2 ) );