let G be RealNormSpace-Sequence; 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; 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); 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); ( y = (reproj (i,x)) . xi & i <> j implies (proj j) . x = (proj j) . y )
assume A1:
( y = (reproj (i,x)) . xi & i <> j )
; (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; verum