( len <*a,b*> = 2 & len <*c,d*> = 2 ) by FINSEQ_1:61;
hence <*<*a,b*>,<*c,d*>*> is tabular FinSequence by MATRIX_1:4; :: thesis: verum