let Fr be XFinSequence of ; :: thesis: ( dom Fr = 0 implies Sum Fr = 0 )
assume dom Fr = 0 ; :: thesis: Sum Fr = 0
then len Fr = 0 ;
hence Sum Fr = 0 by BINOP_2:2, STIRL2_1:def 3; :: thesis: verum