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;
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 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;
now :: thesis: for x being VECTOR of X
for 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;
hence for x being VECTOR of X
for y being VECTOR of Y holds h . (x,y) = (f . (x,y)) - (g . (x,y)) ; :: thesis: verum
end;
assume A2: for x being VECTOR of X
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)
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;
then f = h + g by Th35;
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