let X be RealLinearSpace-Sequence; :: thesis: for Y being RealLinearSpace
for g being MultilinearOperator of X,Y
for t being Point of (product X)
for s being Element of product (carr X) st s = t & ex i being Element of dom X st s . i = 0. (X . i) holds
g . t = 0. Y
let Y be RealLinearSpace; :: thesis: for g being MultilinearOperator of X,Y
for t being Point of (product X)
for s being Element of product (carr X) st s = t & ex i being Element of dom X st s . i = 0. (X . i) holds
g . t = 0. Y
let g be MultilinearOperator of X,Y; :: thesis: for t being Point of (product X)
for s being Element of product (carr X) st s = t & ex i being Element of dom X st s . i = 0. (X . i) holds
g . t = 0. Y
let t be Point of (product X); :: thesis: for s being Element of product (carr X) st s = t & ex i being Element of dom X st s . i = 0. (X . i) holds
g . t = 0. Y
let s be Element of product (carr X); :: thesis: ( s = t & ex i being Element of dom X st s . i = 0. (X . i) implies g . t = 0. Y )
assume that
A1: s = t and
A2: ex i being Element of dom X st s . i = 0. (X . i) ; :: thesis: g . t = 0. Y
consider i being Element of dom X such that
A3: s . i = 0. (X . i) by A2;
A7: (g * (reproj (i,t))) . (0. (X . i)) = g . ((reproj (i,t)) . (0. (X . i))) by FUNCT_2:15
.= g . t by A1, A3, Th4X ;
g * (reproj (i,t)) is LinearOperator of (X . i),Y by Def3;
hence g . t = 0. Y by A7, LOPBAN73; :: thesis: verum