:: deftheorem defines # CARDFIL3:def 1 :
for I being set
for Y being non empty set
for x being b₂ -valued ManySortedSet of I
for p being FinSequence of I holds # (p,x) = p * x;