deffunc H₁( 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₁(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