set W = MultilinearOperators (X,Y);
A1: for v, u being VECTOR of (RealVectSpace ( the carrier of (product X),Y)) st v in MultilinearOperators (X,Y) & u in MultilinearOperators (X,Y) holds
v + u in MultilinearOperators (X,Y)

proof

let v, u be VECTOR of (RealVectSpace ( the carrier of (product X),Y)); :: thesis: ( v in MultilinearOperators (X,Y) & u in MultilinearOperators (X,Y) implies v + u in MultilinearOperators (X,Y) )
assume that
A2: v in MultilinearOperators (X,Y) and
A3: u in MultilinearOperators (X,Y) ; :: thesis: v + u in MultilinearOperators (X,Y)
reconsider u1 = u as MultilinearOperator of X,Y by A3, Def6;
reconsider v1 = v as MultilinearOperator of X,Y by A2, Def6;
v + u is MultilinearOperator of X,Y

proof

reconsider L0 = v + u as Function of (product X),Y by FUNCT_2:66;

now :: thesis: for i being Element of dom X
for x being Point of (product X) holds L0 * (reproj (i,x)) is LinearOperator of (X . i),Y

let i be Element of dom X; :: thesis: for x being Point of (product X) holds L0 * (reproj (i,x)) is LinearOperator of (X . i),Y
let x be Point of (product X); :: thesis: L0 * (reproj (i,x)) is LinearOperator of (X . i),Y
reconsider L = L0 * (reproj (i,x)) as Function of (X . i),Y ;
A4: ( u1 * (reproj (i,x)) is LinearOperator of (X . i),Y & v1 * (reproj (i,x)) is LinearOperator of (X . i),Y ) by Def3;
A5: for x1, x2 being Point of (X . i) holds L . (x1 + x2) = (L . x1) + (L . x2)

proof

let x1, x2 be Point of (X . i); :: thesis: L . (x1 + x2) = (L . x1) + (L . x2)
thus L . (x1 + x2) = L0 . ((reproj (i,x)) . (x1 + x2)) by FUNCT_2:15
.= (u1 . ((reproj (i,x)) . (x1 + x2))) + (v1 . ((reproj (i,x)) . (x1 + x2))) by LOPBAN_1:1
.= ((u1 * (reproj (i,x))) . (x1 + x2)) + (v1 . ((reproj (i,x)) . (x1 + x2))) by FUNCT_2:15
.= ((u1 * (reproj (i,x))) . (x1 + x2)) + ((v1 * (reproj (i,x))) . (x1 + x2)) by FUNCT_2:15
.= (((u1 * (reproj (i,x))) . x1) + ((u1 * (reproj (i,x))) . x2)) + ((v1 * (reproj (i,x))) . (x1 + x2)) by A4, VECTSP_1:def 20
.= (((u1 * (reproj (i,x))) . x1) + ((u1 * (reproj (i,x))) . x2)) + (((v1 * (reproj (i,x))) . x1) + ((v1 * (reproj (i,x))) . x2)) by A4, VECTSP_1:def 20
.= (((u1 * (reproj (i,x))) . x1) + ((v1 * (reproj (i,x))) . x1)) + (((u1 * (reproj (i,x))) . x2) + ((v1 * (reproj (i,x))) . x2)) by LM14
.= ((u1 . ((reproj (i,x)) . x1)) + ((v1 * (reproj (i,x))) . x1)) + (((u1 * (reproj (i,x))) . x2) + ((v1 * (reproj (i,x))) . x2)) by FUNCT_2:15
.= ((u1 . ((reproj (i,x)) . x1)) + (v1 . ((reproj (i,x)) . x1))) + (((u1 * (reproj (i,x))) . x2) + ((v1 * (reproj (i,x))) . x2)) by FUNCT_2:15
.= ((u1 . ((reproj (i,x)) . x1)) + (v1 . ((reproj (i,x)) . x1))) + ((u1 . ((reproj (i,x)) . x2)) + ((v1 * (reproj (i,x))) . x2)) by FUNCT_2:15
.= ((u1 . ((reproj (i,x)) . x1)) + (v1 . ((reproj (i,x)) . x1))) + ((u1 . ((reproj (i,x)) . x2)) + (v1 . ((reproj (i,x)) . x2))) by FUNCT_2:15
.= (L0 . ((reproj (i,x)) . x1)) + ((u1 . ((reproj (i,x)) . x2)) + (v1 . ((reproj (i,x)) . x2))) by LOPBAN_1:1
.= (L0 . ((reproj (i,x)) . x1)) + (L0 . ((reproj (i,x)) . x2)) by LOPBAN_1:1
.= (L . x1) + ((u + v) . ((reproj (i,x)) . x2)) by FUNCT_2:15
.= (L . x1) + (L . x2) by FUNCT_2:15 ; :: thesis: verum

end;

for x being Point of (X . i)
for a being Real holds L . (a * x) = a * (L . x)

proof

let x1 be Point of (X . i); :: thesis: for a being Real holds L . (a * x1) = a * (L . x1)
let a be Real; :: thesis: L . (a * x1) = a * (L . x1)
thus L . (a * x1) = L0 . ((reproj (i,x)) . (a * x1)) by FUNCT_2:15
.= (u1 . ((reproj (i,x)) . (a * x1))) + (v1 . ((reproj (i,x)) . (a * x1))) by LOPBAN_1:1
.= ((u1 * (reproj (i,x))) . (a * x1)) + (v1 . ((reproj (i,x)) . (a * x1))) by FUNCT_2:15
.= ((u1 * (reproj (i,x))) . (a * x1)) + ((v1 * (reproj (i,x))) . (a * x1)) by FUNCT_2:15
.= (a * ((u1 * (reproj (i,x))) . x1)) + ((v1 * (reproj (i,x))) . (a * x1)) by A4, LOPBAN_1:def 5
.= (a * ((u1 * (reproj (i,x))) . x1)) + (a * ((v1 * (reproj (i,x))) . x1)) by A4, LOPBAN_1:def 5
.= (a * (u1 . ((reproj (i,x)) . x1))) + (a * ((v1 * (reproj (i,x))) . x1)) by FUNCT_2:15
.= (a * (u1 . ((reproj (i,x)) . x1))) + (a * (v1 . ((reproj (i,x)) . x1))) by FUNCT_2:15
.= a * ((u1 . ((reproj (i,x)) . x1)) + (v1 . ((reproj (i,x)) . x1))) by RLVECT_1:def 5
.= a * (L0 . ((reproj (i,x)) . x1)) by LOPBAN_1:1
.= a * (L . x1) by FUNCT_2:15 ; :: thesis: verum

end;

hence L0 * (reproj (i,x)) is LinearOperator of (X . i),Y by A5, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: verum

end;

hence v + u is MultilinearOperator of X,Y by Def3; :: thesis: verum

end;

hence v + u in MultilinearOperators (X,Y) by Def6; :: thesis: verum

end;

for b being Real
for v being VECTOR of (RealVectSpace ( the carrier of (product X),Y)) st v in MultilinearOperators (X,Y) holds
b * v in MultilinearOperators (X,Y)

proof

let b be Real; :: thesis: for v being VECTOR of (RealVectSpace ( the carrier of (product X),Y)) st v in MultilinearOperators (X,Y) holds
b * v in MultilinearOperators (X,Y)
let v be VECTOR of (RealVectSpace ( the carrier of (product X),Y)); :: thesis: ( v in MultilinearOperators (X,Y) implies b * v in MultilinearOperators (X,Y) )
assume A9: v in MultilinearOperators (X,Y) ; :: thesis: b * v in MultilinearOperators (X,Y)
reconsider v1 = v as MultilinearOperator of X,Y by A9, Def6;
b * v is MultilinearOperator of X,Y

proof

reconsider L0 = b * v as Function of (product X),Y by FUNCT_2:66;

now :: thesis: for i being Element of dom X
for x being Point of (product X) holds L0 * (reproj (i,x)) is LinearOperator of (X . i),Y

let i be Element of dom X; :: thesis: for x being Point of (product X) holds L0 * (reproj (i,x)) is LinearOperator of (X . i),Y
let x be Point of (product X); :: thesis: L0 * (reproj (i,x)) is LinearOperator of (X . i),Y
reconsider L = L0 * (reproj (i,x)) as Function of (X . i),Y ;
A10: v1 * (reproj (i,x)) is LinearOperator of (X . i),Y by Def3;
A11: for x1, x2 being Point of (X . i) holds L . (x1 + x2) = (L . x1) + (L . x2)

proof

let x1, x2 be Point of (X . i); :: thesis: L . (x1 + x2) = (L . x1) + (L . x2)
thus L . (x1 + x2) = L0 . ((reproj (i,x)) . (x1 + x2)) by FUNCT_2:15
.= b * (v1 . ((reproj (i,x)) . (x1 + x2))) by LOPBAN_1:2
.= b * ((v1 * (reproj (i,x))) . (x1 + x2)) by FUNCT_2:15
.= b * (((v1 * (reproj (i,x))) . x1) + ((v1 * (reproj (i,x))) . x2)) by A10, VECTSP_1:def 20
.= (b * ((v1 * (reproj (i,x))) . x1)) + (b * ((v1 * (reproj (i,x))) . x2)) by RLVECT_1:def 5
.= (b * (v1 . ((reproj (i,x)) . x1))) + (b * ((v1 * (reproj (i,x))) . x2)) by FUNCT_2:15
.= (b * (v1 . ((reproj (i,x)) . x1))) + (b * (v1 . ((reproj (i,x)) . x2))) by FUNCT_2:15
.= (L0 . ((reproj (i,x)) . x1)) + (b * (v1 . ((reproj (i,x)) . x2))) by LOPBAN_1:2
.= (L0 . ((reproj (i,x)) . x1)) + (L0 . ((reproj (i,x)) . x2)) by LOPBAN_1:2
.= (L . x1) + (L0 . ((reproj (i,x)) . x2)) by FUNCT_2:15
.= (L . x1) + (L . x2) by FUNCT_2:15 ; :: thesis: verum

end;

for z being Point of (X . i)
for a being Real holds L . (a * z) = a * (L . z)

proof

let x1 be Point of (X . i); :: thesis: for a being Real holds L . (a * x1) = a * (L . x1)
let a be Real; :: thesis: L . (a * x1) = a * (L . x1)
thus L . (a * x1) = L0 . ((reproj (i,x)) . (a * x1)) by FUNCT_2:15
.= b * (v1 . ((reproj (i,x)) . (a * x1))) by LOPBAN_1:2
.= b * ((v1 * (reproj (i,x))) . (a * x1)) by FUNCT_2:15
.= b * (a * ((v1 * (reproj (i,x))) . x1)) by A10, LOPBAN_1:def 5
.= (b * a) * ((v1 * (reproj (i,x))) . x1) by RLVECT_1:def 7
.= a * (b * ((v1 * (reproj (i,x))) . x1)) by RLVECT_1:def 7
.= a * (b * (v1 . ((reproj (i,x)) . x1))) by FUNCT_2:15
.= a * (L0 . ((reproj (i,x)) . x1)) by LOPBAN_1:2
.= a * (L . x1) by FUNCT_2:15 ; :: thesis: verum

end;

hence L0 * (reproj (i,x)) is LinearOperator of (X . i),Y by A11, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: verum

end;

hence b * v is MultilinearOperator of X,Y by Def3; :: thesis: verum

end;

hence b * v in MultilinearOperators (X,Y) by Def6; :: thesis: verum

end;

hence MultilinearOperators (X,Y) is linearly-closed by A1, RLSUB_1:def 1; :: thesis: verum