set g = the carrier of (product X) --> (0. Y);
take
the carrier of (product X) --> (0. Y)
; the carrier of (product X) --> (0. Y) is Multilinear
now 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),Ylet i be
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),Ylet x be
Element of
(product X);
( the carrier of (product X) --> (0. Y)) * (reproj (i,x)) is LinearOperator of (X . i),Yset F =
( the carrier of (product X) --> (0. Y)) * (reproj (i,x));
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
then
( the carrier of (product X) --> (0. Y)) * (reproj (i,x)) = (dom (( the carrier of (product X) --> (0. Y)) * (reproj (i,x)))) --> (0. Y)
by FUNCOP_1:11;
then A4:
( the carrier of (product X) --> (0. Y)) * (reproj (i,x)) = the
carrier of
(X . i) --> (0. Y)
by FUNCT_2:def 1;
reconsider f =
( the carrier of (product X) --> (0. Y)) * (reproj (i,x)) as
Function of the
carrier of
(X . i),
Y ;
A5:
now for x, y being VECTOR of (X . i) holds f . (x + y) = (f . x) + (f . y)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;
verum end;
hence
the carrier of (product X) --> (0. Y) is Multilinear
; verum