let G be RealLinearSpace-Sequence; :: thesis: for i being Element of dom G
for x being Element of (product G)
for r being Element of (G . i) holds (reproj (i,x)) . r = x +* (i,r)
let i be Element of dom G; :: thesis: for x being Element of (product G)
for r being Element of (G . i) holds (reproj (i,x)) . r = x +* (i,r)
let x be Element of (product G); :: thesis: for r being Element of (G . i) holds (reproj (i,x)) . r = x +* (i,r)
ex x0 being Element of product (carr G) st
( x0 = x & reproj (i,x) = reproj (i,x0) ) by LOPBAN10:def 2;
hence for r being Element of (G . i) holds (reproj (i,x)) . r = x +* (i,r) by LOPBAN10:def 1; :: thesis: verum