let G be non-trivial 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
A4: ( (reproj (i,x)) . v = x +* (i,v) & (reproj (i,y)) . v = y +* (i,v) ) by Def5;
reconsider xv = (reproj (i,x)) . v, yv = (reproj (i,y)) . v as len G -element FinSequence ;
A5: ( dom xv = Seg (len G) & dom yv = Seg (len G) ) by FINSEQ_1:89;
then AA: 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 PA: k in dom xv ; :: thesis: xv . k = yv . k
( x in the carrier of (product G) & y in the carrier of (product G) ) ;
then PP: ( x in product (carr G) & y in product (carr G) ) by LM001;
then consider g being Function such that
P1: ( x = g & dom g = dom (carr G) & ( for i being set st i in dom (carr G) holds
g . i in (carr G) . i ) ) by CARD_3:def 5;
consider g1 being Function such that
P2: ( y = g1 & dom g1 = dom (carr G) & ( for i being set st i in dom (carr G) holds
g1 . i in (carr G) . i ) ) by PP, CARD_3:def 5;
Z1: ( k in dom y & k in dom x ) by P1, P2, ZE, PA, AA;

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 Z1, FUNCT_7:31;
hence yv . k = xv . k by A4; :: thesis: verum

end;

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

A8: ( yv . k = y . k & xv . k = x . k ) by A4, Z, FUNCT_7:32;
y = x +* (i,xi) by A1, Def5;
hence yv . k = xv . k by A8, Z, FUNCT_7:32; :: thesis: verum

end;

end;

end;

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

end;

hence reproj (i,x) = reproj (i,y) by FUNCT_2:def 8; :: thesis: verum