let X be non empty MetrSpace; :: thesis: for x being Element of X ex S being sequence of X st rng S = {x}
let x be Element of X; :: thesis: ex S being sequence of X st rng S = {x}
consider f being Function such that
A1: dom f = NAT and
A2: rng f = {x} by FUNCT_1:5;
reconsider f = f as sequence of X by A1, A2, FUNCT_2:2;
take f ; :: thesis: rng f = {x}
thus rng f = {x} by A2; :: thesis: verum