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

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