let X, Y, Z be RealNormSpace; :: thesis: for f, g, h being Point of (R_NormSpace_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 Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)); :: thesis: ( 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)) )

reconsider f9 = f, g9 = g, h9 = h as Lipschitzian BilinearOperator of X,Y,Z by Def9;

for y being VECTOR of Y holds h . (x,y) = (f . (x,y)) - (g . (x,y)) ; :: thesis: h = f - g

then f - g = h + (g - g) by RLVECT_1:def 3;

then f - g = h + (0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))) by RLVECT_1:15;

hence h = f - g ; :: thesis: verum

( 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 Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)); :: thesis: ( 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)) )

reconsider f9 = f, g9 = g, h9 = h as Lipschitzian BilinearOperator of X,Y,Z by Def9;

hereby :: thesis: ( ( 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:
for x being VECTOR of Xfor y being VECTOR of Y holds h . (x,y) = (f . (x,y)) - (g . (x,y)) ) implies h = f - g )

assume
h = f - g
; :: thesis: for x being VECTOR of X

for y being VECTOR of Y holds h . (x,y) = (f . (x,y)) - (g . (x,y))

then h + g = f - (g - g) by RLVECT_1:29;

then A1: h + g = f - (0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))) by RLVECT_1:15;

for y being VECTOR of Y holds h . (x,y) = (f . (x,y)) - (g . (x,y)) ; :: thesis: verum

end;for y being VECTOR of Y holds h . (x,y) = (f . (x,y)) - (g . (x,y))

then h + g = f - (g - g) by RLVECT_1:29;

then A1: h + g = f - (0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))) by RLVECT_1:15;

now :: thesis: for x being VECTOR of X

for y being VECTOR of Y holds (f9 . (x,y)) - (g9 . (x,y)) = h9 . (x,y)

hence
for x being VECTOR of Xfor y being VECTOR of Y holds (f9 . (x,y)) - (g9 . (x,y)) = h9 . (x,y)

let x be VECTOR of X; :: thesis: for y being VECTOR of Y holds (f9 . (x,y)) - (g9 . (x,y)) = h9 . (x,y)

let y be VECTOR of Y; :: thesis: (f9 . (x,y)) - (g9 . (x,y)) = h9 . (x,y)

f9 . (x,y) = (h9 . (x,y)) + (g9 . (x,y)) by A1, Th35;

then (f9 . (x,y)) - (g9 . (x,y)) = (h9 . (x,y)) + ((g9 . (x,y)) - (g9 . (x,y))) by RLVECT_1:def 3;

then (f9 . (x,y)) - (g9 . (x,y)) = (h9 . (x,y)) + (0. Z) by RLVECT_1:15;

hence (f9 . (x,y)) - (g9 . (x,y)) = h9 . (x,y) ; :: thesis: verum

end;let y be VECTOR of Y; :: thesis: (f9 . (x,y)) - (g9 . (x,y)) = h9 . (x,y)

f9 . (x,y) = (h9 . (x,y)) + (g9 . (x,y)) by A1, Th35;

then (f9 . (x,y)) - (g9 . (x,y)) = (h9 . (x,y)) + ((g9 . (x,y)) - (g9 . (x,y))) by RLVECT_1:def 3;

then (f9 . (x,y)) - (g9 . (x,y)) = (h9 . (x,y)) + (0. Z) by RLVECT_1:15;

hence (f9 . (x,y)) - (g9 . (x,y)) = h9 . (x,y) ; :: thesis: verum

for y being VECTOR of Y holds h . (x,y) = (f . (x,y)) - (g . (x,y)) ; :: thesis: verum

for y being VECTOR of Y holds h . (x,y) = (f . (x,y)) - (g . (x,y)) ; :: thesis: h = f - g

now :: thesis: for x being VECTOR of X

for y being VECTOR of Y holds (h9 . (x,y)) + (g9 . (x,y)) = f9 . (x,y)

then
f = h + g
by Th35;for y being VECTOR of Y holds (h9 . (x,y)) + (g9 . (x,y)) = f9 . (x,y)

let x be VECTOR of X; :: thesis: for y being VECTOR of Y holds (h9 . (x,y)) + (g9 . (x,y)) = f9 . (x,y)

let y be VECTOR of Y; :: thesis: (h9 . (x,y)) + (g9 . (x,y)) = f9 . (x,y)

h9 . (x,y) = (f9 . (x,y)) - (g9 . (x,y)) by A2;

then (h9 . (x,y)) + (g9 . (x,y)) = (f9 . (x,y)) - ((g9 . (x,y)) - (g9 . (x,y))) by RLVECT_1:29;

then (h9 . (x,y)) + (g9 . (x,y)) = (f9 . (x,y)) - (0. Z) by RLVECT_1:15;

hence (h9 . (x,y)) + (g9 . (x,y)) = f9 . (x,y) ; :: thesis: verum

end;let y be VECTOR of Y; :: thesis: (h9 . (x,y)) + (g9 . (x,y)) = f9 . (x,y)

h9 . (x,y) = (f9 . (x,y)) - (g9 . (x,y)) by A2;

then (h9 . (x,y)) + (g9 . (x,y)) = (f9 . (x,y)) - ((g9 . (x,y)) - (g9 . (x,y))) by RLVECT_1:29;

then (h9 . (x,y)) + (g9 . (x,y)) = (f9 . (x,y)) - (0. Z) by RLVECT_1:15;

hence (h9 . (x,y)) + (g9 . (x,y)) = f9 . (x,y) ; :: thesis: verum

then f - g = h + (g - g) by RLVECT_1:def 3;

then f - g = h + (0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))) by RLVECT_1:15;

hence h = f - g ; :: thesis: verum