theorem :: HILB10_7:58

for F being FinSequence-yielding FinSequence
for f being FinSequence holds card (doms (F ^ <*f*>)) = (card (doms F)) * (len f)