let X, Y, Z be RealNormSpace; for f, g, h being VECTOR of (R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) holds
( h = f + g iff for x being VECTOR of X
for y being VECTOR of Y holds h . (x,y) = (f . (x,y)) + (g . (x,y)) )
let f, g, h be VECTOR of (R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)); ( h = f + g iff for x being VECTOR of X
for y being VECTOR of Y holds h . (x,y) = (f . (x,y)) + (g . (x,y)) )
A1:
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is Subspace of R_VectorSpace_of_BilinearOperators (X,Y,Z)
by RSSPACE:11;
then reconsider f1 = f as VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by RLSUB_1:10;
reconsider h1 = h as VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by A1, RLSUB_1:10;
reconsider g1 = g as VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by A1, RLSUB_1:10;
hereby ( ( for x being VECTOR of X
for y being VECTOR of Y holds h . (x,y) = (f . (x,y)) + (g . (x,y)) ) implies h = f + g )
assume A2:
h = f + g
;
for x being Element of X
for y being Element of Y holds h . (x,y) = (f . (x,y)) + (g . (x,y))let x be
Element of
X;
for y being Element of Y holds h . (x,y) = (f . (x,y)) + (g . (x,y))let y be
Element of
Y;
h . (x,y) = (f . (x,y)) + (g . (x,y))
h1 = f1 + g1
by A1, A2, RLSUB_1:13;
hence
h . (
x,
y)
= (f . (x,y)) + (g . (x,y))
by Th16;
verum
end;
assume
for x being Element of X
for y being Element of Y holds h . (x,y) = (f . (x,y)) + (g . (x,y))
; h = f + g
then
h1 = f1 + g1
by Th16;
hence
h = f + g
by A1, RLSUB_1:13; verum