thus len <*x*> = 1 by Th57; :: according to FINSEQ_1:def 18 :: thesis: verum