let b be complex-valued FinSequence; :: thesis: ( len b = 1 implies Product b = b . 1 )
assume len b = 1 ; :: thesis: Product b = b . 1
then b = <*(b . 1)*> by FINSEQ_1:40;
hence Product b = b . 1 by RVSUM_1:95; :: thesis: verum