let G be RealNormSpace-Sequence; :: thesis: for i, j being Element of dom G
for x, y being Point of (product G)
for xi being Point of (G . i) st y = (reproj (i,x)) . xi & i <> j holds
(proj j) . x = (proj j) . y
let i, j be Element of dom G; :: thesis: for x, y being Point of (product G)
for xi being Point of (G . i) st y = (reproj (i,x)) . xi & i <> j holds
(proj j) . x = (proj j) . y
let x, y be Point of (product G); :: thesis: for xi being Point of (G . i) st y = (reproj (i,x)) . xi & i <> j holds
(proj j) . x = (proj j) . y
let xi be Point of (G . i); :: thesis: ( y = (reproj (i,x)) . xi & i <> j implies (proj j) . x = (proj j) . y )
assume A1: ( y = (reproj (i,x)) . xi & i <> j ) ; :: thesis: (proj j) . x = (proj j) . y
reconsider y1 = y as Element of product (carr G) by Th10;
A2: y = x +* (i,xi) by A1, Def4;
set ix = i .--> xi;
A3: the carrier of (product G) = product (carr G) by Th10;
y1 . j = x . j by A2, A1, FUNCT_7:32;
then (proj j) . y = x . j by Def3;
hence (proj j) . x = (proj j) . y by A3, Def3; :: thesis: verum