theorem Th1: :: MSAFREE5:10

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