len (<%> COMPLEX) = 0 ;
hence for f being empty XFinSequence holds XProduct f = 1 by BINOP_2:6, AFINSQ_2:def 8; :: thesis: verum