let X be RealNormSpace-Sequence; for Y being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of (product X) holds h . x = (f . x) + (g . x) )
let Y be RealNormSpace; for f, g, h being VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of (product X) holds h . x = (f . x) + (g . x) )
let f, g, h be VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y)); ( h = f + g iff for x being VECTOR of (product X) holds h . x = (f . x) + (g . x) )
reconsider f9 = f, g9 = g, h9 = h as MultilinearOperator of X,Y by Def6;
A1:
R_VectorSpace_of_MultilinearOperators (X,Y) is Subspace of RealVectSpace ( the carrier of (product X),Y)
by RSSPACE:11;
then reconsider f1 = f, h1 = h, g1 = g as VECTOR of (RealVectSpace ( the carrier of (product X),Y)) by RLSUB_1:10;
hence
( h = f + g iff for x being VECTOR of (product X) holds h . x = (f . x) + (g . x) )
by A2; verum