B1: for i being Nat st i in dom f holds
0 <= f . i by PosDef;
ex i being Nat st
( i in dom f & 0 < f . i )
proof
take i = 1; :: thesis: ( i in dom f & 0 < f . i )
1 in dom f by FINSEQ_5:6;
hence ( i in dom f & 0 < f . i ) by PosDef; :: thesis: verum
end;
then Sum f > 0 by B1, RVSUM_1:85;
hence Mean f is positive ; :: thesis: verum