let G be RealNormSpace-Sequence; :: thesis: 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; :: thesis: 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); :: thesis: (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)

proof

let j be Element of dom G; :: thesis: v . j = (s . j) - (t . j)

per cases ( i = j or i <> j ) ;

suppose A1: i = j ; :: thesis: v . j = (s . j) - (t . j)

then reconsider yy = y as Point of (G . j) ;
v . j = x - y by Th33, A1;
then v . j = (s . j) - yy by Th33, A1;
hence v . j = (s . j) - (t . j) by Th33, A1; :: thesis: verum

end;

suppose A2: i <> j ; :: thesis: v . j = (s . j) - (t . j)

then v . j = 0. (G . j) by Th33;
then v . j = (0. (G . j)) - (0. (G . j)) by RLVECT_1:13;
then v . j = (s . j) - (0. (G . j)) by Th33, A2;
hence v . j = (s . j) - (t . j) by Th33, A2; :: thesis: verum

end;

end;

end;

hence (reproj (i,(0. (product G)))) . (x - y) = ((reproj (i,(0. (product G)))) . x) - ((reproj (i,(0. (product G)))) . y) by Th15; :: thesis: verum