let f be complex-valued FinSequence; :: thesis: for g being FinSequence of F_Complex st f = g holds
Product f = Product g
let g be FinSequence of F_Complex; :: thesis: ( f = g implies Product f = Product g )
A1: ex F being FinSequence of COMPLEX st
( f = F & Product f = multcomplex $$ F ) by RVSUM_1:def 13;
the multF of F_Complex = multcomplex by COMPLFLD:def 1;
hence ( f = g implies Product f = Product g ) by A1, COMPLFLD:def 1; :: thesis: verum