let c be Complex; :: thesis: for f being complex-valued Function holds c (#) f = ((dom f) --> c) (#) f
let f be complex-valued Function; :: thesis: c (#) f = ((dom f) --> c) (#) f
set g = (dom f) --> c;
A2: dom (c (#) f) = dom f by VALUED_1:def 5;
thus A3: dom (c (#) f) = (dom ((dom f) --> c)) /\ (dom f) by VALUED_1:def 5
.= dom (((dom f) --> c) (#) f) by VALUED_1:def 4 ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (c (#) f) or (c (#) f) . b₁ = (((dom f) --> c) (#) f) . b₁ )
let x be object ; :: thesis: ( not x in dom (c (#) f) or (c (#) f) . x = (((dom f) --> c) (#) f) . x )
assume A4: x in dom (c (#) f) ; :: thesis: (c (#) f) . x = (((dom f) --> c) (#) f) . x
then A5: ((dom f) --> c) . x = c by A2, FUNCOP_1:7;
thus (c (#) f) . x = c * (f . x) by VALUED_1:6
.= (((dom f) --> c) (#) f) . x by A3, A4, A5, VALUED_1:def 4 ; :: thesis: verum