let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL

for r being Real st f is V82() holds

r (#) f is V82()

let f be PartFunc of C,ExtREAL; :: thesis: for r being Real st f is V82() holds

r (#) f is V82()

let r be Real; :: thesis: ( f is V82() implies r (#) f is V82() )

assume A1: f is V82() ; :: thesis: r (#) f is V82()

for x being Element of C st x in dom (r (#) f) holds

|.((r (#) f) . x).| < +infty

for r being Real st f is V82() holds

r (#) f is V82()

let f be PartFunc of C,ExtREAL; :: thesis: for r being Real st f is V82() holds

r (#) f is V82()

let r be Real; :: thesis: ( f is V82() implies r (#) f is V82() )

assume A1: f is V82() ; :: thesis: r (#) f is V82()

for x being Element of C st x in dom (r (#) f) holds

|.((r (#) f) . x).| < +infty

proof

hence
r (#) f is V82()
; :: thesis: verum
let x be Element of C; :: thesis: ( x in dom (r (#) f) implies |.((r (#) f) . x).| < +infty )

assume A2: x in dom (r (#) f) ; :: thesis: |.((r (#) f) . x).| < +infty

then x in dom f by MESFUNC1:def 6;

then A3: |.(f . x).| < +infty by A1;

then - +infty < f . x by EXTREAL1:21;

then A4: -infty < f . x by XXREAL_3:def 3;

f . x < +infty by A3, EXTREAL1:21;

then reconsider y = f . x as Element of REAL by A4, XXREAL_0:14;

reconsider yy = f . x as Element of ExtREAL ;

reconsider ry = r * y as Element of REAL by XREAL_0:def 1;

A5: -infty < ry by XXREAL_0:12;

A6: ry < +infty by XXREAL_0:9;

A7: -infty < r * y by A5;

A8: r * y = r * yy by XXREAL_3:def 5

.= (r (#) f) . x by A2, MESFUNC1:def 6 ;

then A9: - +infty < (r (#) f) . x by A7, XXREAL_3:def 3;

(r (#) f) . x < +infty by A6, A8;

hence |.((r (#) f) . x).| < +infty by A9, EXTREAL1:22; :: thesis: verum

end;assume A2: x in dom (r (#) f) ; :: thesis: |.((r (#) f) . x).| < +infty

then x in dom f by MESFUNC1:def 6;

then A3: |.(f . x).| < +infty by A1;

then - +infty < f . x by EXTREAL1:21;

then A4: -infty < f . x by XXREAL_3:def 3;

f . x < +infty by A3, EXTREAL1:21;

then reconsider y = f . x as Element of REAL by A4, XXREAL_0:14;

reconsider yy = f . x as Element of ExtREAL ;

reconsider ry = r * y as Element of REAL by XREAL_0:def 1;

A5: -infty < ry by XXREAL_0:12;

A6: ry < +infty by XXREAL_0:9;

A7: -infty < r * y by A5;

A8: r * y = r * yy by XXREAL_3:def 5

.= (r (#) f) . x by A2, MESFUNC1:def 6 ;

then A9: - +infty < (r (#) f) . x by A7, XXREAL_3:def 3;

(r (#) f) . x < +infty by A6, A8;

hence |.((r (#) f) . x).| < +infty by A9, EXTREAL1:22; :: thesis: verum