:: deftheorem defines index DIST_2:def 1 :
for S being non empty finite set
for a being Element of S holds index a = a .. (canFS S);