let G be RealNormSpace-Sequence; :: thesis: for i 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 holds
reproj (i,x) = reproj (i,y)
let i 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 holds
reproj (i,x) = reproj (i,y)
let x, y be Point of (product G); :: thesis: for xi being Point of (G . i) st y = (reproj (i,x)) . xi holds
reproj (i,x) = reproj (i,y)
let xi be Point of (G . i); :: thesis: ( y = (reproj (i,x)) . xi implies reproj (i,x) = reproj (i,y) )
assume A1: y = (reproj (i,x)) . xi ; :: thesis: reproj (i,x) = reproj (i,y)
for v being Element of (G . i) holds (reproj (i,x)) . v = (reproj (i,y)) . v

proof

let v be Element of (G . i); :: thesis: (reproj (i,x)) . v = (reproj (i,y)) . v
A2: ( (reproj (i,x)) . v = x +* (i,v) & (reproj (i,y)) . v = y +* (i,v) ) by Def4;
reconsider xv = (reproj (i,x)) . v, yv = (reproj (i,y)) . v as len G -element FinSequence ;
A3: ( dom xv = Seg (len G) & dom yv = Seg (len G) ) by FINSEQ_1:89;
then A4: dom xv = dom G by FINSEQ_1:def 3;
for k being Nat st k in dom xv holds
xv . k = yv . k

proof

let k be Nat; :: thesis: ( k in dom xv implies xv . k = yv . k )
assume A5: k in dom xv ; :: thesis: xv . k = yv . k
( x in the carrier of (product G) & y in the carrier of (product G) ) ;
then A6: ( x in product (carr G) & y in product (carr G) ) by Th10;
then consider g being Function such that
A7: ( x = g & dom g = dom (carr G) & ( for i being object st i in dom (carr G) holds
g . i in (carr G) . i ) ) by CARD_3:def 5;
consider g1 being Function such that
A8: ( y = g1 & dom g1 = dom (carr G) & ( for i being object st i in dom (carr G) holds
g1 . i in (carr G) . i ) ) by A6, CARD_3:def 5;
A9: ( k in dom y & k in dom x ) by A7, A8, Lm1, A5, A4;

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

suppose k = i ; :: thesis: xv . k = yv . k

then ( (y +* (i,v)) . k = v & (x +* (i,v)) . k = v ) by A9, FUNCT_7:31;
hence yv . k = xv . k by A2; :: thesis: verum

end;

suppose A10: k <> i ; :: thesis: xv . k = yv . k

A11: ( yv . k = y . k & xv . k = x . k ) by A2, A10, FUNCT_7:32;
y = x +* (i,xi) by A1, Def4;
hence yv . k = xv . k by A11, A10, FUNCT_7:32; :: thesis: verum

end;

end;

end;

hence (reproj (i,x)) . v = (reproj (i,y)) . v by A3, FINSEQ_1:13; :: thesis: verum

end;

hence reproj (i,x) = reproj (i,y) ; :: thesis: verum