let G be non-trivial RealNormSpace-Sequence; :: thesis: for i, j being Element of dom G
for x being Point of (G . i)
for z being Element of product (carr G) st z = (reproj (i,(0. (product G)))) . x holds
( ( i = j implies z . j = x ) & ( i <> j implies z . j = 0. (G . j) ) )
let i, j be Element of dom G; :: thesis: for x being Point of (G . i)
for z being Element of product (carr G) st z = (reproj (i,(0. (product G)))) . x holds
( ( i = j implies z . j = x ) & ( i <> j implies z . j = 0. (G . j) ) )
let x be Point of (G . i); :: thesis: for z being Element of product (carr G) st z = (reproj (i,(0. (product G)))) . x holds
( ( i = j implies z . j = x ) & ( i <> j implies z . j = 0. (G . j) ) )
let z be Element of product (carr G); :: thesis: ( z = (reproj (i,(0. (product G)))) . x implies ( ( i = j implies z . j = x ) & ( i <> j implies z . j = 0. (G . j) ) ) )
assume AS: z = (reproj (i,(0. (product G)))) . x ; :: thesis: ( ( i = j implies z . j = x ) & ( i <> j implies z . j = 0. (G . j) ) )
reconsider Zr = 0. (product G) as Element of product (carr G) by LM001;
reconsider ixr = (reproj (i,(0. (product G)))) . x as Element of product (carr G) by LM001;
X9: (reproj (i,(0. (product G)))) . x = (0. (product G)) +* (i,x) by Def5;
set ix = i .--> x;
consider g being Function such that
P1: ( Zr = 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;
S1: dom Zr = dom G by P1, ZE;

now

assume i <> j ; :: thesis: z . j = 0. (G . j)
then z . j = Zr . j by AS, X9, FUNCT_7:32;
hence z . j = 0. (G . j) by ZR1; :: thesis: verum

end;

hence ( ( i = j implies z . j = x ) & ( i <> j implies z . j = 0. (G . j) ) ) by AS, X9, S1, FUNCT_7:31; :: thesis: verum