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