take f = seq_const 0; :: thesis: ( f is summable & f is constant & f is convergent )
for n being Nat holds f . n = 0 ;
hence f is summable by RSSPACE:16; :: thesis: ( f is constant & f is convergent )
thus f is constant ; :: thesis: f is convergent
thus f is convergent ; :: thesis: verum