let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace holds the carrier of (product X) --> (0. Y) is MultilinearOperator of X,Y
let Y be RealNormSpace; :: thesis: the carrier of (product X) --> (0. Y) is MultilinearOperator of X,Y
set f0 = the carrier of (product X) --> (0. Y);

now :: thesis: for i being Element of dom X
for u being Element of (product X) holds ( the carrier of (product X) --> (0. Y)) * (reproj (i,u)) is LinearOperator of (X . i),Y

let i be Element of dom X; :: thesis: for u being Element of (product X) holds ( the carrier of (product X) --> (0. Y)) * (reproj (i,u)) is LinearOperator of (X . i),Y
let u be Element of (product X); :: thesis: ( the carrier of (product X) --> (0. Y)) * (reproj (i,u)) is LinearOperator of (X . i),Y
set F = ( the carrier of (product X) --> (0. Y)) * (reproj (i,u));
A1: dom (( the carrier of (product X) --> (0. Y)) * (reproj (i,u))) = the carrier of (X . i) by FUNCT_2:def 1;
A4: for z being object st z in dom (( the carrier of (product X) --> (0. Y)) * (reproj (i,u))) holds
(( the carrier of (product X) --> (0. Y)) * (reproj (i,u))) . z = 0. Y

proof

let z be object ; :: thesis: ( z in dom (( the carrier of (product X) --> (0. Y)) * (reproj (i,u))) implies (( the carrier of (product X) --> (0. Y)) * (reproj (i,u))) . z = 0. Y )
assume z in dom (( the carrier of (product X) --> (0. Y)) * (reproj (i,u))) ; :: thesis: (( the carrier of (product X) --> (0. Y)) * (reproj (i,u))) . z = 0. Y
then A2: z in the carrier of (X . i) by FUNCT_2:def 1;
thus (( the carrier of (product X) --> (0. Y)) * (reproj (i,u))) . z = ( the carrier of (product X) --> (0. Y)) . ((reproj (i,u)) . z) by A2, FUNCT_2:15
.= 0. Y by A2, FUNCT_2:5, FUNCOP_1:7 ; :: thesis: verum

end;

reconsider f = ( the carrier of (product X) --> (0. Y)) * (reproj (i,u)) as Function of (X . i),Y ;
A5: f is homogeneous

proof

let x be VECTOR of (X . i); :: according to LOPBAN_1:def 5 :: thesis: for b₁ being object holds f . (b₁ * x) = b₁ * (f . x)
let r be Real; :: thesis: f . (r * x) = r * (f . x)
thus f . (r * x) = r * (0. Y) by A1, A4
.= r * (f . x) by A1, A4 ; :: thesis: verum

end;

now :: thesis: for x, y being VECTOR of (X . i) holds f . (x + y) = (f . x) + (f . y)

let x, y be VECTOR of (X . i); :: thesis: f . (x + y) = (f . x) + (f . y)
thus f . (x + y) = 0. Y by A1, A4
.= (f . x) + (0. Y) by A1, A4
.= (f . x) + (f . y) by A1, A4 ; :: thesis: verum

end;

hence ( the carrier of (product X) --> (0. Y)) * (reproj (i,u)) is LinearOperator of (X . i),Y by A5, VECTSP_1:def 20; :: thesis: verum

end;

hence the carrier of (product X) --> (0. Y) is MultilinearOperator of X,Y by Def3; :: thesis: verum