let G be non-trivial 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 LM001;
X3: dom (carr G) = dom G by ZE;
reconsider Zr = 0. (product G) as Element of product (carr G) by LM001;
reconsider ixr = (reproj (i,x)) . r as Element of product (carr G) by LM001;
reconsider p = ((reproj (i,x)) . r) - x as Element of product (carr G) by LM001;
X5: dom p = dom (carr G) by CARD_3:9;
reconsider q = (reproj (i,(0. (product G)))) . (r - ((proj i) . x)) as Element of product (carr G) by LM001;
X6: dom q = dom (carr G) by CARD_3:9;
reconsider s = x - ((reproj (i,x)) . r) as Element of product (carr G) by LM001;
X7: dom s = dom (carr G) by CARD_3:9;
reconsider t = (reproj (i,(0. (product G)))) . (((proj i) . x) - r) as Element of product (carr G) by LM001;
X8: dom t = dom (carr G) by CARD_3:9;
X9: (reproj (i,x)) . r = x +* (i,r) by Def5;
reconsider xfi = xf . i as Point of (G . i) ;
(reproj (i,(0. (product G)))) . (r - ((proj i) . x)) = (0. (product G)) +* (i,(r - ((proj i) . x))) by Def5;
then X11: q = Zr +* (i,(r - xfi)) by Def1;
(reproj (i,(0. (product G)))) . (((proj i) . x) - r) = (0. (product G)) +* (i,(((proj i) . x) - r)) by Def5;
then X12: t = Zr +* (i,(xfi - r)) by Def1;
set ir = i .--> r;
set irx1 = i .--> (r - xfi);
set irx2 = i .--> (xfi - r);
x in the carrier of (product G) ;
then p0: x in product (carr G) by LM001;
consider g1 being Function such that
p1: ( x = g1 & dom g1 = dom (carr G) & ( for i being set st i in dom (carr G) holds
g1 . i in (carr G) . i ) ) by p0, CARD_3:def 5;
for k being set st k in dom p holds
p . k = q . k

proof

let k be set ; :: thesis: ( k in dom p implies p . k = q . k )
assume S1: k in dom p ; :: thesis: p . k = q . k
then reconsider k0 = k as Element of dom G by X3, CARD_3:9;
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;
F1: k in dom Zr by P1, S1, CARD_3:9;
F2: k in dom x by p1, S1, CARD_3:9;

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

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

then Z: k <> i by TARSKI:def 1;
then XA3: q . k0 = Zr . k0 by X11, FUNCT_7:32;
p . k = (ixr . k0) - (xf . k0) by SUB1
.= (xf . k0) - (xf . k0) by Z, X9, FUNCT_7:32 ;
then p . k = 0. (G . k0) by RLVECT_1:15;
hence p . k = q . k by XA3, ZR1; :: thesis: verum

end;

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

then XA5: k = i by TARSKI:def 1;
then XA6: q . k0 = r - xfi by X11, F1, FUNCT_7:31;
p . k = (ixr . k0) - (xf . k0) by SUB1;
hence p . k = q . k by XA6, X9, XA5, F2, FUNCT_7:31; :: thesis: verum

end;

end;

end;

hence ((reproj (i,x)) . r) - x = (reproj (i,(0. (product G)))) . (r - ((proj i) . x)) by X5, X6, FUNCT_1:2; :: thesis: x - ((reproj (i,x)) . r) = (reproj (i,(0. (product G)))) . (((proj i) . x) - r)
for k being set st k in dom s holds
s . k = t . k

proof

let k be set ; :: thesis: ( k in dom s implies s . k = t . k )
assume P0: k in dom s ; :: thesis: s . k = t . k
then reconsider k0 = k as Element of dom G by X3, CARD_3:9;
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;
F1: k in dom Zr by P1, P0, CARD_3:9;
F2: k in dom x by p1, P0, CARD_3:9;

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

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

then Z: k <> i by TARSKI:def 1;
then XA3: t . k0 = Zr . k0 by X12, FUNCT_7:32;
s . k = (xf . k0) - (ixr . k0) by SUB1
.= (xf . k0) - (xf . k0) by X9, Z, FUNCT_7:32 ;
then s . k = 0. (G . k0) by RLVECT_1:15;
hence s . k = t . k by XA3, ZR1; :: thesis: verum

end;

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

then XA5: k = i by TARSKI:def 1;
then XA6: t . k0 = xfi - r by X12, F1, FUNCT_7:31;
s . k = (xf . k0) - (ixr . k0) by SUB1;
hence s . k = t . k by XA6, X9, XA5, F2, FUNCT_7:31; :: thesis: verum

end;

end;

end;

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