:: deftheorem defines diff PENCIL_3:def 1 :
for I being non empty finite set
for b1, b2 being ManySortedSet of I holds diff (b1,b2) = card { i where i is Element of I : b1 . i <> b2 . i } ;