theorem Th14: :: MATRIXJ1:14

for D being non empty set
for F1, F2 being FinSequence_of_Matrix of D holds Len (F1 ^ F2) = (Len F1) ^ (Len F2)