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 A2: x in dom f ; :: thesis: |.(f . x).| < +infty
A3: f . x in rng f by A2, FUNCT_1:12;
A4: rng f c= REAL by A1, VALUED_0:def 3;
thus |.(f . x).| < +infty by A3, A4, EXTREAL2:102; :: thesis: verum

end;

assume A5: for x being Element of X st x in dom f holds
|.(f . x).| < +infty ; :: thesis: f is real-valued
let e be set ; :: according to VALUED_0:def 9 :: thesis: ( not e in proj1 f or f . e is real )
assume A6: e in dom f ; :: thesis: f . e is real
reconsider x = e as Element of X by A6;
A7: |.(f . x).| < +infty by A5, A6;
A8: f . x in REAL by A7, EXTREAL2:102;
thus f . e is real by A8; :: thesis: verum