let X be non empty set ; :: thesis: for Y being RealLinearSpace ex MULT being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st
for r being Real
for f being Element of Funcs (X, the carrier of Y)
for s being Element of X holds (MULT . [r,f]) . s = r * (f . s)
let Y be RealLinearSpace; :: thesis: ex MULT being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st
for r being Real
for f being Element of Funcs (X, the carrier of Y)
for s being Element of X holds (MULT . [r,f]) . s = r * (f . s)
deffunc H₁( Real, 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 [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) such that
A1: for a being Real
for f being Element of Funcs (X, the carrier of Y) holds F . (a,f) = H₁(a,f) from BINOP_1:sch 4();
take F ; :: thesis: for r being Real
for f being Element of Funcs (X, the carrier of Y)
for s being Element of X holds (F . [r,f]) . s = r * (f . s)
let a be Real; :: thesis: for f being Element of Funcs (X, the carrier of Y)
for s being Element of X holds (F . [a,f]) . s = a * (f . s)
let f be Element of Funcs (X, the carrier of Y); :: thesis: for s being Element of X holds (F . [a,f]) . s = a * (f . s)
let x be Element of X; :: thesis: (F . [a,f]) . x = a * (f . x)
A2: dom (F . [a,f]) = X by FUNCT_2:169;
F . (a,f) = the Mult of Y [;] (a,f) by A1;
hence (F . [a,f]) . x = a * (f . x) by A2, FUNCOP_1:42; :: thesis: verum