let G be RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for y being Point of (product G)
for q being Point of (G . i) st q = (proj i) . y holds
y = (reproj (i,y)) . q
let i be Element of dom G; :: thesis: for y being Point of (product G)
for q being Point of (G . i) st q = (proj i) . y holds
y = (reproj (i,y)) . q
let y be Point of (product G); :: thesis: for q being Point of (G . i) st q = (proj i) . y holds
y = (reproj (i,y)) . q
let q be Point of (G . i); :: thesis: ( q = (proj i) . y implies y = (reproj (i,y)) . q )
assume A1: q = (proj i) . y ; :: thesis: y = (reproj (i,y)) . q
reconsider z1 = (reproj (i,y)) . q as len G -element FinSequence ;
reconsider z2 = y as len G -element FinSequence ;
A2: dom z1 = Seg (len G) by FINSEQ_1:89
.= dom z2 by FINSEQ_1:89 ;
for k being Nat st k in dom z1 holds
z1 . k = z2 . k

proof

let k be Nat; :: thesis: ( k in dom z1 implies z1 . k = z2 . k )
assume k in dom z1 ; :: thesis: z1 . k = z2 . k
product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
then A3: q = y . i by A1, Def3;

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

suppose A4: k = i ; :: thesis: z1 . k = z2 . k

then (y +* (i,q)) . k = q by A3, FUNCT_7:35;
hence z1 . k = z2 . k by A4, A3, Def4; :: thesis: verum

end;

suppose k <> i ; :: thesis: z1 . k = z2 . k

then (y +* (i,q)) . k = y . k by FUNCT_7:32;
hence z1 . k = z2 . k by Def4; :: thesis: verum

end;

end;

end;

hence y = (reproj (i,y)) . q by A2, FINSEQ_1:13; :: thesis: verum