let a be Real; :: thesis: ex f being constant Function of NAT,REAL st
for x being Nat holds f . x = a
a in REAL by XREAL_0:def 1;
then reconsider Sa = NAT --> a as Function of NAT,REAL by FUNCOP_1:45;
A12: for n being Nat holds Sa . n = a by ORDINAL1:def 12, FUNCOP_1:7;
for x, y being object st x in dom Sa & y in dom Sa holds
Sa . x = Sa . y

proof

let x, y be object ; :: thesis: ( x in dom Sa & y in dom Sa implies Sa . x = Sa . y )
assume ( x in dom Sa & y in dom Sa ) ; :: thesis: Sa . x = Sa . y
then reconsider x0 = x, y0 = y as Element of NAT ;
thus Sa . x = Sa . x0
.= a by A12
.= Sa . y0 by A12
.= Sa . y ; :: thesis: verum

end;

then Sa is constant by FUNCT_1:def 10;
hence ex f being constant Function of NAT,REAL st
for x being Nat holds f . x = a by A12; :: thesis: verum