let X, Y be RealNormSpace; :: thesis: for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )
let f, g, h be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )
reconsider f9 = f, g9 = g, h9 = h as Lipschitzian LinearOperator of X,Y by Def9;
hereby :: thesis: ( ( for x being VECTOR of X holds h . x = (f . x) - (g . x) ) implies h = f - g )
assume h = f - g ; :: thesis: for x being VECTOR of X holds h . x = (f . x) - (g . x)
then h + g = f - (g - g) by RLVECT_1:29;
then h + g = f - (0. (R_NormSpace_of_BoundedLinearOperators (X,Y))) by RLVECT_1:15;
then A1: h + g = f ;
now :: thesis: for x being VECTOR of X holds (f9 . x) - (g9 . x) = h9 . x
let x be VECTOR of X; :: thesis: (f9 . x) - (g9 . x) = h9 . x
f9 . x = (h9 . x) + (g9 . x) by A1, Th35;
then (f9 . x) - (g9 . x) = (h9 . x) + ((g9 . x) - (g9 . x)) by RLVECT_1:def 3;
then (f9 . x) - (g9 . x) = (h9 . x) + (0. Y) by RLVECT_1:15;
hence (f9 . x) - (g9 . x) = h9 . x ; :: thesis: verum
end;
hence for x being VECTOR of X holds h . x = (f . x) - (g . x) ; :: thesis: verum
end;
assume A2: for x being VECTOR of X holds h . x = (f . x) - (g . x) ; :: thesis: h = f - g
now :: thesis: for x being VECTOR of X holds (h9 . x) + (g9 . x) = f9 . x
let x be VECTOR of X; :: thesis: (h9 . x) + (g9 . x) = f9 . x
h9 . x = (f9 . x) - (g9 . x) by A2;
then (h9 . x) + (g9 . x) = (f9 . x) - ((g9 . x) - (g9 . x)) by RLVECT_1:29;
then (h9 . x) + (g9 . x) = (f9 . x) - (0. Y) by RLVECT_1:15;
hence (h9 . x) + (g9 . x) = f9 . x ; :: 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_BoundedLinearOperators (X,Y))) by RLVECT_1:15;
hence h = f - g ; :: thesis: verum