let cF be complex-valued XFinSequence; :: thesis: ( cF = {} implies Product cF = 1 )
assume cF = {} ; :: thesis: Product cF = 1
then len cF = 0 ;
hence Product cF = 1 by BINOP_2:6, AFINSQ_2:def 8; :: thesis: verum