thus ( f is real-valued implies for x being Element of X st x in dom f holds
|.(f . x).| < +infty ) :: thesis: ( ( for x being Element of X st x in dom f holds
|.(f . x).| < +infty ) implies f is real-valued )

proof

assume A1: f is real-valued ; :: thesis: for x being Element of X st x in dom f holds
|.(f . x).| < +infty
let x be Element of X; :: thesis: ( x in dom f implies |.(f . x).| < +infty )
assume x in dom f ; :: thesis: |.(f . x).| < +infty
then A2: f . x in rng f by FUNCT_1:3;
rng f c= REAL by A1;
hence |.(f . x).| < +infty by A2, EXTREAL1:41; :: thesis: verum

end;

assume A3: for x being Element of X st x in dom f holds
|.(f . x).| < +infty ; :: thesis: f is real-valued
let e be object ; :: according to VALUED_0:def 9 :: thesis: ( not e in dom f or not f . e is real )
assume A4: e in dom f ; :: thesis: f . e is real
then reconsider x = e as Element of X ;
|.(f . x).| < +infty by A3, A4;
then f . x in REAL by EXTREAL1:41;
hence f . e is real ; :: thesis: verum