deffunc H_{1}( 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) = H_{1}(c,f)
from BINOP_1:sch 4();

take F ; :: thesis: 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; :: thesis: 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); :: thesis: for x being Element of X holds (F . [c,f]) . x = c * (f . x)

let x be Element of X; :: thesis: (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 ;

:: thesis: verum

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) = H

take F ; :: thesis: 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; :: thesis: 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); :: thesis: for x being Element of X holds (F . [c,f]) . x = c * (f . x)

let x be Element of X; :: thesis: (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 ;

:: thesis: verum