let x be real-valued FinSequence; ( x <> {} & x is positive implies 0 < Sum x )
assume that
A1:
x <> {}
and
A2:
x is positive
; 0 < Sum x
consider i being object such that
A3:
i in dom x
by A1, XBOOLE_0:def 1;
A4:
0 < x . i
by A3, A2;
for i being Nat st i in dom x holds
0 <= x . i
by A2;
hence
0 < Sum x
by RVSUM_1:85, A3, A4; verum