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

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