thus len <*x1,x2,x3,x4*> = 4 by FINSEQ_4:91; :: according to CIRCCOMB:def 12 :: thesis: verum