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
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
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 )
assume A1: r <> 0 ; :: thesis: for c being Element of C st c in dom (r (#) f) holds
f . c = ((r (#) f) . c) / r
let c be Element of C; :: thesis: ( c in dom (r (#) f) implies f . c = ((r (#) f) . c) / r )
assume c in dom (r (#) f) ; :: thesis: f . c = ((r (#) f) . c) / r
then A2: (r (#) f) . c = r * (f . c) by Def6;

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

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

now :: thesis: f . c = ((r (#) f) . c) / r

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

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

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: verum

end;

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

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: verum

end;

end;

end;

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

end;

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

now :: thesis: f . c = ((r (#) f) . c) / r

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

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

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: verum

end;

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

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: verum

end;

end;

end;

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

end;

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

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 by EXTREAL1:2
.= a / (r / r) by XCMPLX_1:77
.= a / 1 by A1, XCMPLX_1:60 ;
hence f . c = ((r (#) f) . c) / r ; :: thesis: verum

end;

end;