deffunc H1( Complex, Element of Funcs (X, the carrier of Y)) -> Element of Funcs (X, the carrier of Y) = the Mult of Y [;] ($1,$2);
consider F being Function of [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) such that
A1:
for c being Element of COMPLEX
for f being Element of Funcs (X, the carrier of Y) holds F . (c,f) = H1(c,f)
from BINOP_1:sch 4();
take
F
; for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (F . [c,f]) . x = c * (f . x)
let c be Complex; for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (F . [c,f]) . x = c * (f . x)
let f be Element of Funcs (X, the carrier of Y); for x being Element of X holds (F . [c,f]) . x = c * (f . x)
let x be Element of X; (F . [c,f]) . x = c * (f . x)
reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2;
A2:
dom (F . [c1,f]) = X
by FUNCT_2:92;
F . (c1,f) = the Mult of Y [;] (c1,f)
by A1;
hence (F . [c,f]) . x =
the Mult of Y . (c,(f . x))
by A2, FUNCOP_1:32
.=
c * (f . x)
by CLVECT_1:def 1
;
verum