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