theorem Th13: :: PRALG_1:14

for p being 1-sorted-yielding FinSequence holds len (Carrier p) = len p