let X be RealNormSpace-Sequence; :: thesis: for i being Element of dom X
for x being Element of (product X) ex x0 being Element of product (carr X) st
( x0 = x & reproj (i,x) = reproj (i,x0) )
let i be Element of dom X; :: thesis: for x being Element of (product X) ex x0 being Element of product (carr X) st
( x0 = x & reproj (i,x) = reproj (i,x0) )
let x be Element of (product X); :: thesis: ex x0 being Element of product (carr X) st
( x0 = x & reproj (i,x) = reproj (i,x0) )
A1: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
then reconsider x0 = x as Element of product (carr X) ;
take x0 ; :: thesis: ( x0 = x & reproj (i,x) = reproj (i,x0) )
A5: (carr X) . i = the carrier of (X . i) by PRVECT_1:def 11;
now :: thesis: for r being Element of (X . i) holds (reproj (i,x)) . r = (reproj (i,x0)) . r
let r be Element of (X . i); :: thesis: (reproj (i,x)) . r = (reproj (i,x0)) . r
thus (reproj (i,x)) . r = x +* (i,r) by NDIFF_5:def 4
.= (reproj (i,x0)) . r by A5, Def1 ; :: thesis: verum
end;
hence ( x0 = x & reproj (i,x) = reproj (i,x0) ) by A1, A5, FUNCT_2:63; :: thesis: verum