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 A1: ( rng a = {r} & rng b = {r} ) ; :: thesis: a = b

now

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

end;

hence a = b by FUNCT_2:113; :: thesis: verum