thus len <*x,y*> = 2 by Th61; :: according to FINSEQ_1:def 18 :: thesis: verum