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

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)

hence
F = G
by BINOP_1:2; :: thesis: verumfor 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;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