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)
F . z,f = multcomplex [;] z,f by A1;
hence (F . [z,f]) . x = multcomplex . z,(f . x) by FUNCOP_1:66
.= z * (f . x) by BINOP_2:def 5 ;
:: thesis: verum