:: deftheorem defines HetSet RVSUM_3:def 4 :
for f being real-valued FinSequence holds HetSet f = { n where n is Nat : ( n in dom f & f . n <> Mean f ) } ;