theorem Th13f: :: FIELD_11:3

for F being Field
for m, n being Ordinal
for b being bag of n st support b = {m} holds
( len (divisors b) = (b . m) + 1 & ( for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag ) )