let X be non empty set ; :: thesis: for Y being ComplexLinearSpace ex MULT being Function of [:COMPLEX ,(Funcs X,the carrier of Y):],(Funcs X,the carrier of Y) st
for c being Complex
for f being Element of Funcs X,the carrier of Y
for s being Element of X holds (MULT . [c,f]) . s = c * (f . s)
let Y be ComplexLinearSpace; :: thesis: ex MULT being Function of [:COMPLEX ,(Funcs X,the carrier of Y):],(Funcs X,the carrier of Y) st
for c being Complex
for f being Element of Funcs X,the carrier of Y
for s being Element of X holds (MULT . [c,f]) . s = c * (f . s)
deffunc H₁( 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 Complex
for f being Element of Funcs X,the carrier of Y holds F . c,f = H₁(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 s being Element of X holds (F . [c,f]) . s = c * (f . s)
let c be Complex; :: thesis: for f being Element of Funcs X,the carrier of Y
for s being Element of X holds (F . [c,f]) . s = c * (f . s)
let f be Element of Funcs X,the carrier of Y; :: thesis: for s being Element of X holds (F . [c,f]) . s = c * (f . s)
let x be Element of X; :: thesis: (F . [c,f]) . x = c * (f . x)
A2: dom (F . [c,f]) = X by FUNCT_2:169;
F . c,f = the Mult of Y [;] c,f by A1;
hence (F . [c,f]) . x = the Mult of Y . c,(f . x) by A2, FUNCOP_1:42
.= c * (f . x) by CLVECT_1:def 1 ;
:: thesis: verum