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
(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
A3: y = x +* (i,xi) by A1, Def5;
x in the carrier of (product G) ;
then x in product (carr G) by LM001;
then consider g being Function such that
AB: ( x = g & dom g = dom (carr G) & ( for y being set st y in dom (carr G) holds
g . y in (carr G) . y ) ) by CARD_3:def 5;
F1: i in dom G ;
AA: i in dom x by ZE, F1, AB;
y is Element of product (carr G) by LM001;
then (proj i) . y = (x +* (i,xi)) . i by A3, Def1;
hence (proj i) . y = xi by FUNCT_7:31, AA; :: thesis: verum