let C be non empty set ; :: thesis:
let f be PartFunc of C,ExtREAL; :: thesis:
let r be Real; :: thesis:
assume A1: r <> 0 ; :: thesis:
let c be Element of C; :: thesis:
assume c in dom (r (#) f) ; :: thesis:
then A2: (r (#) f) . c = r * (f . c) by Def6;

per cases ;

suppose A3: f . c = +infty ; :: thesis:

now :: thesis:

per cases by A1;

suppose A4: 0. < r ; :: thesis:

then (r (#) f) . c = +infty by A2, A3, XXREAL_3:def 5;
hence f . c = ((r (#) f) . c) / r by A3, A4, XXREAL_3:83; :: thesis:

end;

suppose A5: r < 0. ; :: thesis:

then (r (#) f) . c = -infty by A2, A3, XXREAL_3:def 5;
hence f . c = ((r (#) f) . c) / r by A3, A5, XXREAL_3:84; :: thesis:

end;

end;

end;

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

end;

suppose A6: f . c = -infty ; :: thesis:

now :: thesis:

per cases by A1;

suppose A7: 0. < r ; :: thesis:

then (r (#) f) . c = -infty by A2, A6, XXREAL_3:def 5;
hence f . c = ((r (#) f) . c) / r by A6, A7, XXREAL_3:86; :: thesis:

end;

suppose A8: r < 0. ; :: thesis:

then (r (#) f) . c = +infty by A2, A6, XXREAL_3:def 5;
hence f . c = ((r (#) f) . c) / r by A6, A8, XXREAL_3:85; :: thesis:

end;

end;

end;

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

end;

suppose ( f . c <> +infty & f . c <> -infty ) ; :: thesis:

then reconsider a = f . c as Element of REAL by XXREAL_0:14;
reconsider rr = r as R_eal by XXREAL_0:def 1;
(r (#) f) . c = r * a by A2
.= r * a ;
then ((r (#) f) . c) / rr = (r * a) / r
.= a / (r / r) by XCMPLX_1:77
.= a / 1 by A1, XCMPLX_1:60 ;
hence f . c = ((r (#) f) . c) / r ; :: thesis:

end;

end;