set f = NAT --> 0 ;
reconsider f = NAT --> 0 as Real_Sequence by FUNCOP_1:57;
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:13;
hence f is summable by RSSPACE:20; :: thesis: ( f is constant & f is convergent )
thus f is constant ; :: thesis: f is convergent
thus f is convergent ; :: thesis: verum