set g = the carrier of (product X) --> (0. Y);
take the carrier of (product X) --> (0. Y) ; :: thesis: the carrier of (product X) --> (0. Y) is Multilinear

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

let i be Element of dom X; :: thesis: for x being Element of (product X) holds ( the carrier of (product X) --> (0. Y)) * (reproj (i,x)) is LinearOperator of (X . i),Y
let x be Element of (product X); :: thesis: ( the carrier of (product X) --> (0. Y)) * (reproj (i,x)) is LinearOperator of (X . i),Y
set F = ( the carrier of (product X) --> (0. Y)) * (reproj (i,x));
A1: dom (( the carrier of (product X) --> (0. Y)) * (reproj (i,x))) = 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,x))) holds
(( the carrier of (product X) --> (0. Y)) * (reproj (i,x))) . z = 0. Y

proof

let z be object ; :: thesis: ( z in dom (( the carrier of (product X) --> (0. Y)) * (reproj (i,x))) implies (( the carrier of (product X) --> (0. Y)) * (reproj (i,x))) . z = 0. Y )
assume z in dom (( the carrier of (product X) --> (0. Y)) * (reproj (i,x))) ; :: thesis: (( the carrier of (product X) --> (0. Y)) * (reproj (i,x))) . 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,x))) . z = ( the carrier of (product X) --> (0. Y)) . ((reproj (i,x)) . z) by A2, FUNCT_2:15
.= 0. Y by A2, FUNCOP_1:7, FUNCT_2:5 ; :: thesis: verum

end;

reconsider f = ( the carrier of (product X) --> (0. Y)) * (reproj (i,x)) as Function of the carrier of (X . i),Y ;

A5: 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;

now :: thesis: for x being VECTOR of (X . i)
for r being Real holds f . (r * x) = r * (f . x)

let x be VECTOR of (X . i); :: thesis: for r being Real holds f . (r * x) = r * (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;

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

end;

hence the carrier of (product X) --> (0. Y) is Multilinear ; :: thesis: verum