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 A2: (r (#) f) . c = (R_EAL r) * (f . c) by Def6;

now

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_EAL r)

now

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

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

then (r (#) f) . c = +infty by A2, A3, EXTREAL1:def 1;
hence f . c = ((r (#) f) . c) / (R_EAL r) by A3, A4, EXTREAL1:def 2; :: thesis: verum

end;

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

then (r (#) f) . c = -infty by A2, A3, EXTREAL1:def 1;
hence f . c = ((r (#) f) . c) / (R_EAL r) by A3, A5, EXTREAL1:def 2; :: thesis: verum

end;

end;

end;

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

end;

suppose A6: 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 A7: 0. < R_EAL r ; :: thesis: f . c = ((r (#) f) . c) / (R_EAL r)

then (r (#) f) . c = -infty by A2, A6, EXTREAL1:def 1;
hence f . c = ((r (#) f) . c) / (R_EAL r) by A6, A7, EXTREAL1:def 2; :: thesis: verum

end;

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

then (r (#) f) . c = +infty by A2, A6, EXTREAL1:def 1;
hence f . c = ((r (#) f) . c) / (R_EAL r) by A6, A8, EXTREAL1:def 2; :: 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 A2, EXTREAL1:13;
then ((r (#) f) . c) / (R_EAL r) = (r * a) / r by A1, 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;

end;

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