let x be real-valued FinSequence; :: thesis: ( x <> {} & x is positive implies 0 < Sum x )

assume that

A1: x <> {} and

A2: x is positive ; :: thesis: 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; :: thesis: verum

assume that

A1: x <> {} and

A2: x is positive ; :: thesis: 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; :: thesis: verum