let G be 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 A1: 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 Th10;
reconsider ixr = (reproj (i,(0. (product G)))) . x as Element of product (carr G) by Th10;
A2: (reproj (i,(0. (product G)))) . x = (0. (product G)) +* (i,x) by Def4;
set ix = i .--> x;
consider g being Function such that
A3: ( Zr = g & dom g = dom (carr G) & ( for i being object st i in dom (carr G) holds
g . i in (carr G) . i ) ) by CARD_3:def 5;
A4: dom Zr = dom G by A3, Lm1;

now :: thesis: ( i <> j implies z . j = 0. (G . j) )

assume i <> j ; :: thesis: z . j = 0. (G . j)
then z . j = Zr . j by A1, A2, FUNCT_7:32;
hence z . j = 0. (G . j) by Th14; :: thesis: verum

end;

hence ( ( i = j implies z . j = x ) & ( i <> j implies z . j = 0. (G . j) ) ) by A1, A2, A4, FUNCT_7:31; :: thesis: verum