deffunc H₁( Scalar of K, Element of (V . W)) -> Element of (V . W) = $1 * $2;
consider F being Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W) such that
A1: for r being Scalar of K
for S being Element of (V . W) holds F . (r,S) = H₁(r,S) from BINOP_1:sch 4();
take F ; :: thesis: for r being Scalar of K
for S being Element of (V . W) holds F . (r,S) = r * S
thus for r being Scalar of K
for S being Element of (V . W) holds F . (r,S) = r * S by A1; :: thesis: verum