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 (f - r) . c = (f . c) - r
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 (f - r) . c = (f . c) - r
let f be Function of C,D; :: thesis: for r being Complex
for c being Element of C holds (f - r) . c = (f . c) - r
let r be Complex; :: thesis: for c being Element of C holds (f - r) . c = (f . c) - r
dom (f - r) = C by FUNCT_2:def 1;
hence for c being Element of C holds (f - r) . c = (f . c) - r by Def2; :: thesis: verum