thus len <*x,y*> = 2 by FINSEQ_1:61; :: according to CIRCCOMB:def 12 :: thesis: verum