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 )

|.(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 V40() )

assume A4: e in dom f ; :: thesis: f . e is V40()

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 V40() ; :: thesis: verum

|.(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 A3:
for x being Element of X st x in dom f holds
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;|.(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

|.(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 V40() )

assume A4: e in dom f ; :: thesis: f . e is V40()

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 V40() ; :: thesis: verum