thus len <*x*> = 1 by FINSEQ_1:57; :: according to CIRCCOMB:def 12 :: thesis: verum