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

assume cF = {} ; :: thesis: Product cF = 1

then len cF = 0 ;

hence Product cF = 1 by BINOP_2:6, AFINSQ_2:def 8; :: thesis: verum