let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL
for r being Real st r <> 0 holds
for c being Element of C st c in dom (r (#) f) holds
f . c = ((r (#) f) . c) / (R_EAL r)
let f be PartFunc of C,ExtREAL ; :: thesis: for r being Real st r <> 0 holds
for c being Element of C st c in dom (r (#) f) holds
f . c = ((r (#) f) . c) / (R_EAL r)
let r be Real; :: thesis: ( r <> 0 implies for c being Element of C st c in dom (r (#) f) holds
f . c = ((r (#) f) . c) / (R_EAL r) )
assume A1: r <> 0 ; :: thesis: for c being Element of C st c in dom (r (#) f) holds
f . c = ((r (#) f) . c) / (R_EAL r)
let c be Element of C; :: thesis: ( c in dom (r (#) f) implies f . c = ((r (#) f) . c) / (R_EAL r) )
assume c in dom (r (#) f) ; :: thesis: f . c = ((r (#) f) . c) / (R_EAL r)
then A3: (r (#) f) . c = (R_EAL r) * (f . c) by Def6;

per cases ( f . c = +infty or f . c = -infty or ( f . c <> +infty & f . c <> -infty ) ) ;

suppose A4: f . c = +infty ; :: thesis: f . c = ((r (#) f) . c) / (R_EAL r)

now

per cases ( 0. < R_EAL r or R_EAL r < 0. ) by A1;

suppose A6: 0. < R_EAL r ; :: thesis: f . c = ((r (#) f) . c) / (R_EAL r)

then (r (#) f) . c = +infty by A3, A4, XXREAL_3:def 5;
hence f . c = ((r (#) f) . c) / (R_EAL r) by A4, A6, XXREAL_3:94; :: thesis: verum

end;

suppose A9: R_EAL r < 0. ; :: thesis: f . c = ((r (#) f) . c) / (R_EAL r)

then (r (#) f) . c = -infty by A3, A4, XXREAL_3:def 5;
hence f . c = ((r (#) f) . c) / (R_EAL r) by A4, A9, XXREAL_3:95; :: thesis: verum

end;

end;

end;

hence f . c = ((r (#) f) . c) / (R_EAL r) ; :: thesis: verum

end;

suppose A12: f . c = -infty ; :: thesis: f . c = ((r (#) f) . c) / (R_EAL r)

now

per cases ( 0. < R_EAL r or R_EAL r < 0. ) by A1;

suppose A14: 0. < R_EAL r ; :: thesis: f . c = ((r (#) f) . c) / (R_EAL r)

then (r (#) f) . c = -infty by A3, A12, XXREAL_3:def 5;
hence f . c = ((r (#) f) . c) / (R_EAL r) by A12, A14, XXREAL_3:97; :: thesis: verum

end;

suppose A17: R_EAL r < 0. ; :: thesis: f . c = ((r (#) f) . c) / (R_EAL r)

then (r (#) f) . c = +infty by A3, A12, XXREAL_3:def 5;
hence f . c = ((r (#) f) . c) / (R_EAL r) by A12, A17, XXREAL_3:96; :: thesis: verum

end;

end;

end;

hence f . c = ((r (#) f) . c) / (R_EAL r) ; :: thesis: verum

end;

suppose ( f . c <> +infty & f . c <> -infty ) ; :: thesis: f . c = ((r (#) f) . c) / (R_EAL r)

then reconsider a = f . c as Real by XXREAL_0:14;
(r (#) f) . c = r * a by A3, EXTREAL1:13;
then ((r (#) f) . c) / (R_EAL r) = (r * a) / r by EXTREAL1:32
.= a / (r / r) by XCMPLX_1:78
.= a / 1 by A1, XCMPLX_1:60 ;
hence f . c = ((r (#) f) . c) / (R_EAL r) ; :: thesis: verum

end;

end;