theorem Th4: :: MATRIX_0:4

for n being Nat
for s1, s2 being FinSequence st len s1 = n & len s2 = n holds
<*s1,s2*> is tabular