theorem Th73: :: MATRIXJ1:73

for K being Field
for G1, G2 being FinSequence_of_Matrix of K st Width G1 = Len G2 holds
( Len (G1 (#) G2) = Len G1 & Width (G1 (#) G2) = Width G2 )