set f = NAT --> 0;
reconsider f = NAT --> 0 as Real_Sequence by FUNCOP_1:45;
take f ; :: thesis: ( f is summable & f is constant & f is convergent )
for n being Element of NAT holds f . n = 0 by FUNCOP_1:7;
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