let C be non empty set ; :: thesis: for D being non empty complex-membered set
for f being Function of C,D
for r being Complex
for c being Element of C holds (r + f) . c = r + (f . c)
let D be non empty complex-membered set ; :: thesis: for f being Function of C,D
for r being Complex
for c being Element of C holds (r + f) . c = r + (f . c)
let f be Function of C,D; :: thesis: for r being Complex
for c being Element of C holds (r + f) . c = r + (f . c)
let r be Complex; :: thesis: for c being Element of C holds (r + f) . c = r + (f . c)
dom (r + f) = C by FUNCT_2:def 1;
hence for c being Element of C holds (r + f) . c = r + (f . c) by Def2; :: thesis: verum