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 g being Function of C,COMPLEX st ( for c being Element of C holds g . c = r * (f . c) ) holds
g = r (#) f
let D be non empty complex-membered set ; :: thesis: for f being Function of C,D
for r being Complex
for g being Function of C,COMPLEX st ( for c being Element of C holds g . c = r * (f . c) ) holds
g = r (#) f
let f be Function of C,D; :: thesis: for r being Complex
for g being Function of C,COMPLEX st ( for c being Element of C holds g . c = r * (f . c) ) holds
g = r (#) f
let r be Complex; :: thesis: for g being Function of C,COMPLEX st ( for c being Element of C holds g . c = r * (f . c) ) holds
g = r (#) f
let g be Function of C,COMPLEX; :: thesis: ( ( for c being Element of C holds g . c = r * (f . c) ) implies g = r (#) f )
assume A1: for c being Element of C holds g . c = r * (f . c) ; :: thesis: g = r (#) f
let x be Element of C; :: according to FUNCT_2:def 8 :: thesis: g . x = (r (#) f) . x
thus g . x = r * (f . x) by A1
.= (r (#) f) . x by Th6 ; :: thesis: verum