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 A2: c in dom (r (#) f) ; :: thesis: f . c = ((r (#) f) . c) / (R_EAL r)
A3: (r (#) f) . c = (R_EAL r) * (f . c) by A2, 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)

A5: 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)

A7: (r (#) f) . c = +infty by A3, A4, A6, XXREAL_3:def 5;
A8: R_EAL r < +infty by XXREAL_0:9;
thus f . c = ((r (#) f) . c) / (R_EAL r) by A4, A6, A7, A8, XXREAL_3:94; :: thesis: verum

end;

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

A10: (r (#) f) . c = -infty by A3, A4, A9, XXREAL_3:def 5;
A11: R_EAL r > -infty by XXREAL_0:12;
thus f . c = ((r (#) f) . c) / (R_EAL r) by A4, A9, A10, A11, XXREAL_3:95; :: thesis: verum

end;

end;

end;

thus f . c = ((r (#) f) . c) / (R_EAL r) by A5; :: thesis: verum

end;

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

A13: 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)

A15: (r (#) f) . c = -infty by A3, A12, A14, XXREAL_3:def 5;
A16: R_EAL r < +infty by XXREAL_0:9;
thus f . c = ((r (#) f) . c) / (R_EAL r) by A12, A14, A15, A16, XXREAL_3:97; :: thesis: verum

end;

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

A18: (r (#) f) . c = +infty by A3, A12, A17, XXREAL_3:def 5;
A19: R_EAL r > -infty by XXREAL_0:12;
thus f . c = ((r (#) f) . c) / (R_EAL r) by A12, A17, A18, A19, XXREAL_3:96; :: thesis: verum

end;

end;

end;

thus f . c = ((r (#) f) . c) / (R_EAL r) by A13; :: thesis: verum

end;

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

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

end;

end;