let G be RealNormSpace-Sequence; for i being Element of dom G
for x, y being Point of (G . i) holds (reproj (i,(0. (product G)))) . (x - y) = ((reproj (i,(0. (product G)))) . x) - ((reproj (i,(0. (product G)))) . y)
let i be Element of dom G; for x, y being Point of (G . i) holds (reproj (i,(0. (product G)))) . (x - y) = ((reproj (i,(0. (product G)))) . x) - ((reproj (i,(0. (product G)))) . y)
let x, y be Point of (G . i); (reproj (i,(0. (product G)))) . (x - y) = ((reproj (i,(0. (product G)))) . x) - ((reproj (i,(0. (product G)))) . y)
reconsider v = (reproj (i,(0. (product G)))) . (x - y) as Element of product (carr G) by Th10;
reconsider s = (reproj (i,(0. (product G)))) . x as Element of product (carr G) by Th10;
reconsider t = (reproj (i,(0. (product G)))) . y as Element of product (carr G) by Th10;
for j being Element of dom G holds v . j = (s . j) - (t . j)
hence
(reproj (i,(0. (product G)))) . (x - y) = ((reproj (i,(0. (product G)))) . x) - ((reproj (i,(0. (product G)))) . y)
by Th15; verum