let G be RealNormSpace-Sequence; for i being Element of dom G
for x being Point of (product G)
for r being Point of (G . i) holds
( ((reproj (i,x)) . r) - x = (reproj (i,(0. (product G)))) . (r - ((proj i) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0. (product G)))) . (((proj i) . x) - r) )
let i be Element of dom G; for x being Point of (product G)
for r being Point of (G . i) holds
( ((reproj (i,x)) . r) - x = (reproj (i,(0. (product G)))) . (r - ((proj i) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0. (product G)))) . (((proj i) . x) - r) )
let x be Point of (product G); for r being Point of (G . i) holds
( ((reproj (i,x)) . r) - x = (reproj (i,(0. (product G)))) . (r - ((proj i) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0. (product G)))) . (((proj i) . x) - r) )
let r be Point of (G . i); ( ((reproj (i,x)) . r) - x = (reproj (i,(0. (product G)))) . (r - ((proj i) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0. (product G)))) . (((proj i) . x) - r) )
set m = len G;
reconsider xf = x as Element of product (carr G) by Th10;
A1:
dom (carr G) = dom G
by Lm1;
reconsider Zr = 0. (product G) as Element of product (carr G) by Th10;
reconsider ixr = (reproj (i,x)) . r as Element of product (carr G) by Th10;
reconsider p = ((reproj (i,x)) . r) - x as Element of product (carr G) by Th10;
reconsider q = (reproj (i,(0. (product G)))) . (r - ((proj i) . x)) as Element of product (carr G) by Th10;
A3:
dom q = dom (carr G)
by CARD_3:9;
reconsider s = x - ((reproj (i,x)) . r) as Element of product (carr G) by Th10;
reconsider t = (reproj (i,(0. (product G)))) . (((proj i) . x) - r) as Element of product (carr G) by Th10;
A5:
dom t = dom (carr G)
by CARD_3:9;
A6:
(reproj (i,x)) . r = x +* (i,r)
by Def4;
reconsider xfi = xf . i as Point of (G . i) ;
A7:
(reproj (i,(0. (product G)))) . (r - ((proj i) . x)) = (0. (product G)) +* (i,(r - ((proj i) . x)))
by Def4;
then A7a:
q = Zr +* (i,(r - xfi))
by Def3;
A8:
(reproj (i,(0. (product G)))) . (((proj i) . x) - r) = (0. (product G)) +* (i,(((proj i) . x) - r))
by Def4;
then A8a:
t = Zr +* (i,(xfi - r))
by Def3;
set ir = i .--> r;
set irx1 = i .--> (r - xfi);
set irx2 = i .--> (xfi - r);
x in the carrier of (product G)
;
then A9:
x in product (carr G)
by Th10;
consider g1 being Function such that
A10:
( x = g1 & dom g1 = dom (carr G) & ( for i being object st i in dom (carr G) holds
g1 . i in (carr G) . i ) )
by A9, CARD_3:def 5;
for k being object st k in dom p holds
p . k = q . k
hence
((reproj (i,x)) . r) - x = (reproj (i,(0. (product G)))) . (r - ((proj i) . x))
by A3, FUNCT_1:2, CARD_3:9; x - ((reproj (i,x)) . r) = (reproj (i,(0. (product G)))) . (((proj i) . x) - r)
for k being object st k in dom s holds
s . k = t . k
hence
x - ((reproj (i,x)) . r) = (reproj (i,(0. (product G)))) . (((proj i) . x) - r)
by A5, FUNCT_1:2, CARD_3:9; verum