for I being FinSequence-membered set
for p being FinSequence holds card (p ^^ I) = card I