let A be non empty set ; :: thesis: for x being Element of (R_Normed_Algebra_of_BoundedFunctions A) holds x is Function of A,REAL
let x be Element of (R_Normed_Algebra_of_BoundedFunctions A); :: thesis: x is Function of A,REAL
x is Element of BoundedFunctions A ;
then x is Element of Funcs (A,REAL) ;
hence x is Function of A,REAL ; :: thesis: verum