( 1 in dom f & f . 1 = 0 ) by FINSEQ_5:6;
hence Product f is zero by RVSUM_1:103; :: thesis: verum