let F, G be Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W); :: thesis: ( ( for r being Scalar of K
for S being Element of (V . W) holds F . (r,S) = r * S ) & ( for r being Scalar of K
for S being Element of (V . W) holds G . (r,S) = r * S ) implies F = G )
assume that
A2: for r being Scalar of K
for S being Element of (V . W) holds F . (r,S) = r * S and
A3: for r being Scalar of K
for S being Element of (V . W) holds G . (r,S) = r * S ; :: thesis: F = G

now :: thesis: for r being Scalar of K
for S being Element of (V . W) holds F . (r,S) = G . (r,S)

let r be Scalar of K; :: thesis: for S being Element of (V . W) holds F . (r,S) = G . (r,S)
let S be Element of (V . W); :: thesis: F . (r,S) = G . (r,S)
thus F . (r,S) = r * S by A2
.= G . (r,S) by A3 ; :: thesis: verum

end;

hence F = G by BINOP_1:2; :: thesis: verum