deffunc H_{1}( 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_{1}(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

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

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