let f be complex-valued Function; :: thesis: for r being Complex
for c being object holds (r (#) f) . c = r * (f . c)
let r be Complex; :: thesis: for c being object holds (r (#) f) . c = r * (f . c)
let c be object ; :: thesis: (r (#) f) . c = r * (f . c)
A1: dom f = dom (r (#) f) by Def5;

per cases ( c in dom f or not c in dom f ) ;

suppose c in dom f ; :: thesis: (r (#) f) . c = r * (f . c)

hence (r (#) f) . c = r * (f . c) by A1, Def5; :: thesis: verum

end;

suppose A2: not c in dom f ; :: thesis: (r (#) f) . c = r * (f . c)

hence (r (#) f) . c = r * 0 by A1, FUNCT_1:def 2
.= r * (f . c) by A2, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;