thus len <*x,y,z*> = 3 by Th62; :: according to FINSEQ_1:def 18 :: thesis: verum