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
(proj i) . y = xi
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
(proj i) . y = xi
let x, y be Point of (product G); :: thesis: for xi being Point of (G . i) st y = (reproj (i,x)) . xi holds
(proj i) . y = xi
let xi be Point of (G . i); :: thesis: ( y = (reproj (i,x)) . xi implies (proj i) . y = xi )
assume A1: y = (reproj (i,x)) . xi ; :: thesis: (proj i) . y = xi
A2: y = x +* (i,xi) by A1, Def4;
x in the carrier of (product G) ;
then x in product (carr G) by Th10;
then consider g being Function such that
A3: ( x = g & dom g = dom (carr G) & ( for y being object st y in dom (carr G) holds
g . y in (carr G) . y ) ) by CARD_3:def 5;
A4: i in dom G ;
A5: i in dom x by Lm1, A4, A3;
y is Element of product (carr G) by Th10;
then (proj i) . y = (x +* (i,xi)) . i by A2, Def3;
hence (proj i) . y = xi by A5, FUNCT_7:31; :: thesis: verum