let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace
for g being MultilinearOperator of X,Y
for t being Point of (product X) st ex i being Element of dom X st t . i = 0. (X . i) holds
g . t = 0. Y
let Y be RealNormSpace; :: thesis: for g being MultilinearOperator of X,Y
for t being Point of (product X) st ex i being Element of dom X st t . i = 0. (X . i) holds
g . t = 0. Y
let g be MultilinearOperator of X,Y; :: thesis: for t being Point of (product X) st ex i being Element of dom X st t . i = 0. (X . i) holds
g . t = 0. Y
let t be Point of (product X); :: thesis: ( ex i being Element of dom X st t . i = 0. (X . i) implies g . t = 0. Y )
given i being Element of dom X such that A2: t . i = 0. (X . i) ; :: thesis: g . t = 0. Y
A6: (g * (reproj (i,t))) . (0. (X . i)) = g . ((reproj (i,t)) . (0. (X . i))) by FUNCT_2:15
.= g . t by A2, Th4X ;
g * (reproj (i,t)) is LinearOperator of (X . i),Y by Def3;
hence g . t = 0. Y by A6, LOPBAN_7:3; :: thesis: verum