for D being set
for f being FinSequence of D *
for i being Nat holds Card (f | i) = (Card f) | i