let r be Real; :: thesis: for a, b being Real_Sequence st rng a = {r} & rng b = {r} holds
a = b
let a, b be Real_Sequence; :: thesis: ( rng a = {r} & rng b = {r} implies a = b )
assume that
A1: rng a = {r} and
A2: rng b = {r} ; :: thesis: a = b

now :: thesis: for n being Element of NAT holds a . n = b . n

let n be Element of NAT ; :: thesis: a . n = b . n
a . n in rng a by VALUED_0:28;
then A3: a . n = r by A1, TARSKI:def 1;
b . n in rng b by VALUED_0:28;
hence a . n = b . n by A2, A3, TARSKI:def 1; :: thesis: verum

end;

hence a = b ; :: thesis: verum