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));
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;
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 :: 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) + (0. Y) by A4, FUNCOP_1:7
.= (f . x) + (0. Y) by A4, FUNCOP_1:7
.= (f . x) + (f . y) by A4, FUNCOP_1:7 ; :: 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 A4, FUNCOP_1:7
.= r * (f . x) by A4, FUNCOP_1:7 ; :: 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