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