let F, G be Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W); ( ( 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
; F = G
now 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;
for S being Element of (V . W) holds F . (r,S) = G . (r,S)let S be
Element of
(V . W);
F . (r,S) = G . (r,S)thus F . (
r,
S) =
r * S
by A2
.=
G . (
r,
S)
by A3
;
verum end;
hence
F = G
by BINOP_1:2; verum