thus len <*x1,x2,x3,x4*> = 4 by Th91; :: according to FINSEQ_1:def 18 :: thesis: verum