theorem :: HILB10_7:57

for g being FinSequence holds card (doms <*g*>) = len g