let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace
for f being MultilinearOperator of X,Y holds f . (0. (product X)) = 0. Y
let Y be RealNormSpace; :: thesis: for f being MultilinearOperator of X,Y holds f . (0. (product X)) = 0. Y
let f be MultilinearOperator of X,Y; :: thesis: f . (0. (product X)) = 0. Y
A1: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
reconsider z = 0. (product X) as Element of product (carr X) by A1;
set i = the Element of dom X;
z . the Element of dom X = 0. (X . the Element of dom X) by ZERXI;
hence f . (0. (product X)) = 0. Y by LOPBAN10:36; :: thesis: verum