deffunc H₁( Element of the carrier of R, Element of Funcs ( the carrier of M, the carrier of N)) -> Element of Funcs ( the carrier of M, the carrier of N) = the lmult of N [;] ($1,$2);
consider F1 being Function of [: the carrier of R,(Funcs ( the carrier of M, the carrier of N)):],(Funcs ( the carrier of M, the carrier of N)) such that
A1: for a being Element of the carrier of R
for f being Element of Funcs ( the carrier of M, the carrier of N) holds F1 . (a,f) = H₁(a,f) from BINOP_1:sch 4();
take F1 ; :: thesis: for a being Element of the carrier of R
for f being Element of Funcs ( the carrier of M, the carrier of N)
for x being Element of the carrier of M holds (F1 . [a,f]) . x = a * (f . x)
let a be Element of the carrier of R; :: thesis: for f being Element of Funcs ( the carrier of M, the carrier of N)
for x being Element of the carrier of M holds (F1 . [a,f]) . x = a * (f . x)
let f be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: for x being Element of the carrier of M holds (F1 . [a,f]) . x = a * (f . x)
let x be Element of the carrier of M; :: thesis: (F1 . [a,f]) . x = a * (f . x)
A2: dom (F1 . [a,f]) = the carrier of M by FUNCT_2:92;
F1 . (a,f) = the lmult of N [;] (a,f) by A1;
hence (F1 . [a,f]) . x = a * (f . x) by A2, FUNCOP_1:32; :: thesis: verum