theorem Th17: :: MATRIXJ1:17

for n being Nat
for D being non empty set
for F1 being FinSequence_of_Matrix of D holds Len (F1 | n) = (Len F1) | n