deffunc H_{1}( Element of COMPLEX , Element of Funcs (A,COMPLEX)) -> Element of Funcs (A,COMPLEX) = multcomplex [;] ($1,$2);

consider F being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) such that

A1: for z being Element of COMPLEX

for f being Element of Funcs (A,COMPLEX) holds F . (z,f) = H_{1}(z,f)
from BINOP_1:sch 4();

take F ; :: thesis: for z being Complex

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (F . [z,f]) . x = z * (f . x)

let z be Complex; :: thesis: for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (F . [z,f]) . x = z * (f . x)

let f be Element of Funcs (A,COMPLEX); :: thesis: for x being Element of A holds (F . [z,f]) . x = z * (f . x)

let x be Element of A; :: thesis: (F . [z,f]) . x = z * (f . x)

A2: z in COMPLEX by XCMPLX_0:def 2;

then F . (z,f) = multcomplex [;] (z,f) by A1;

hence (F . [z,f]) . x = multcomplex . (z,(f . x)) by FUNCOP_1:53, A2

.= z * (f . x) by BINOP_2:def 5 ;

:: thesis: verum

consider F being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) such that

A1: for z being Element of COMPLEX

for f being Element of Funcs (A,COMPLEX) holds F . (z,f) = H

take F ; :: thesis: for z being Complex

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (F . [z,f]) . x = z * (f . x)

let z be Complex; :: thesis: for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (F . [z,f]) . x = z * (f . x)

let f be Element of Funcs (A,COMPLEX); :: thesis: for x being Element of A holds (F . [z,f]) . x = z * (f . x)

let x be Element of A; :: thesis: (F . [z,f]) . x = z * (f . x)

A2: z in COMPLEX by XCMPLX_0:def 2;

then F . (z,f) = multcomplex [;] (z,f) by A1;

hence (F . [z,f]) . x = multcomplex . (z,(f . x)) by FUNCOP_1:53, A2

.= z * (f . x) by BINOP_2:def 5 ;

:: thesis: verum