let G be RealNormSpace-Sequence; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( ((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

proof

let k be object ; :: thesis: ( k in dom p implies p . k = q . k )
assume A11: k in dom p ; :: thesis: p . k = q . k
then reconsider k0 = k as Element of dom G by A1, CARD_3:9;
consider g being Function such that
A12: ( 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;
A13: k in dom Zr by A12, A11, CARD_3:9;
A14: k in dom x by A10, A11, CARD_3:9;

per cases ( not k in {i} or k in {i} ) ;

suppose not k in {i} ; :: thesis: p . k = q . k

then A15: k <> i by TARSKI:def 1;
then A16: q . k0 = Zr . k0 by A7, FUNCT_7:32;
p . k = (ixr . k0) - (xf . k0) by Th15
.= (xf . k0) - (xf . k0) by A15, A6, FUNCT_7:32 ;
then p . k = 0. (G . k0) by RLVECT_1:15;
hence p . k = q . k by A16, Th14; :: thesis: verum

end;

suppose k in {i} ; :: thesis: p . k = q . k

then A17: k = i by TARSKI:def 1;
then A18: q . k0 = r - xfi by A7a, A13, FUNCT_7:31;
p . k = (ixr . k0) - (xf . k0) by Th15;
hence p . k = q . k by A18, A6, A17, A14, FUNCT_7:31; :: thesis: verum

end;

end;

end;

hence ((reproj (i,x)) . r) - x = (reproj (i,(0. (product G)))) . (r - ((proj i) . x)) by A3, FUNCT_1:2, CARD_3:9; :: thesis: 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

proof

let k be object ; :: thesis: ( k in dom s implies s . k = t . k )
assume A19: k in dom s ; :: thesis: s . k = t . k
then reconsider k0 = k as Element of dom G by A1, CARD_3:9;
consider g being Function such that
A20: ( 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;
A21: k in dom Zr by A20, A19, CARD_3:9;
A22: k in dom x by A10, A19, CARD_3:9;

per cases ( not k in {i} or k in {i} ) ;

suppose not k in {i} ; :: thesis: s . k = t . k

then A23: k <> i by TARSKI:def 1;
then A24: t . k0 = Zr . k0 by A8, FUNCT_7:32;
s . k = (xf . k0) - (ixr . k0) by Th15
.= (xf . k0) - (xf . k0) by A6, A23, FUNCT_7:32 ;
then s . k = 0. (G . k0) by RLVECT_1:15;
hence s . k = t . k by A24, Th14; :: thesis: verum

end;

suppose k in {i} ; :: thesis: s . k = t . k

then A25: k = i by TARSKI:def 1;
then A26: t . k0 = xfi - r by A8a, A21, FUNCT_7:31;
s . k = (xf . k0) - (ixr . k0) by Th15;
hence s . k = t . k by A26, A6, A25, A22, FUNCT_7:31; :: thesis: verum

end;

end;

end;

hence x - ((reproj (i,x)) . r) = (reproj (i,(0. (product G)))) . (((proj i) . x) - r) by A5, FUNCT_1:2, CARD_3:9; :: thesis: verum