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

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