let G be non-trivial RealNormSpace-Sequence; :: thesis: for h being FinSequence of (product G)
for y, x being Point of (product G)
for y0, Z being Element of product (carr G)
for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds
((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. (j + 1)))) = (proj (modetrans (G,(((len G) + 1) -' j)))) . y
let h be FinSequence of (product G); :: thesis: for y, x being Point of (product G)
for y0, Z being Element of product (carr G)
for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds
((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. (j + 1)))) = (proj (modetrans (G,(((len G) + 1) -' j)))) . y
let y, x be Point of (product G); :: thesis: for y0, Z being Element of product (carr G)
for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds
((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. (j + 1)))) = (proj (modetrans (G,(((len G) + 1) -' j)))) . y
let y0, Z be Element of product (carr G); :: thesis: for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds
((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. (j + 1)))) = (proj (modetrans (G,(((len G) + 1) -' j)))) . y
let j be Element of NAT ; :: thesis: ( y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) implies ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. (j + 1)))) = (proj (modetrans (G,(((len G) + 1) -' j)))) . y )
assume that
A1: y = y0 and
A2: Z = 0. (product G) and
A3: ( len h = (len G) + 1 & 1 <= j & j <= len G ) and
A4: for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ; :: thesis: ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. (j + 1)))) = (proj (modetrans (G,(((len G) + 1) -' j)))) . y
x + (h /. j) = (reproj ((modetrans (G,(((len G) + 1) -' j))),(x + (h /. (j + 1))))) . ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) by A1, A2, A3, A4, Th46;
then (proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. j)) = (proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y) by XTh39;
then A6: ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. (j + 1)))) = (proj (modetrans (G,(((len G) + 1) -' j)))) . ((x + (h /. j)) - (x + (h /. (j + 1)))) by YTh9M;
(x + (h /. j)) - (x + (h /. (j + 1))) = (((h /. j) + x) - x) - (h /. (j + 1)) by RLVECT_1:27
.= ((h /. j) + (x - x)) - (h /. (j + 1)) by RLVECT_1:28
.= ((h /. j) + (0. (product G))) - (h /. (j + 1)) by RLVECT_1:15
.= (h /. j) - (h /. (j + 1)) by RLVECT_1:4 ;
then A7: ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. (j + 1)))) = ((proj (modetrans (G,(((len G) + 1) -' j)))) . (h /. j)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (h /. (j + 1))) by A6, YTh9M;
y0 is Element of the carrier of (product G) by LM001;
then B1: dom y0 = Seg (len G) by FINSEQ_1:89;
j in Seg (len G) by A3;
then ((len G) -' j) + 1 in Seg (len G) by NAT_2:6;
then B2: ((len G) + 1) -' j in Seg (len G) by A3, NAT_D:38;
A8: j < (len G) + 1 by A3, NAT_1:13;
then ((len G) + 1) -' j in Seg (((len G) + 1) -' j) by FINSEQ_1:3, NAT_D:36;
then B5: ((len G) + 1) -' j in dom (y0 | (Seg (((len G) + 1) -' j))) by B1, B2, RELAT_1:57;
((len G) + 1) -' j = (((len G) + 1) -' (j + 1)) + 1 by A8, NAT_2:7;
then C1: ((len G) + 1) -' (j + 1) < ((len G) + 1) -' j by NAT_1:13;
dom (y0 | (Seg (((len G) + 1) -' (j + 1)))) c= Seg (((len G) + 1) -' (j + 1)) by RELAT_1:58;
then C3: not ((len G) + 1) -' j in dom (y0 | (Seg (((len G) + 1) -' (j + 1)))) by C1, FINSEQ_1:1;
reconsider h1 = h /. j as Element of product (carr G) by LM001;
reconsider h2 = h /. (j + 1) as Element of product (carr G) by LM001;
j in Seg (len h) by A3, A8;
then j in dom h by FINSEQ_1:def 3;
then B6: h /. j = Z +* (y0 | (Seg (((len G) + 1) -' j))) by A4;
((len G) + 1) -' j in dom G by B2, FINSEQ_1:def 3;
then B3: modetrans (G,(((len G) + 1) -' j)) = ((len G) + 1) -' j by Defmode;
then B7: (proj (modetrans (G,(((len G) + 1) -' j)))) . (h /. j) = h1 . (((len G) + 1) -' j) by Def1
.= (y0 | (Seg (((len G) + 1) -' j))) . (((len G) + 1) -' j) by B5, B6, FUNCT_4:13
.= y0 . (((len G) + 1) -' j) by B5, FUNCT_1:47
.= (proj (modetrans (G,(((len G) + 1) -' j)))) . y by A1, B3, Def1 ;
( 1 <= j + 1 & j + 1 <= len h ) by A3, NAT_1:12, XREAL_1:6;
then j + 1 in Seg (len h) ;
then j + 1 in dom h by FINSEQ_1:def 3;
then B8: h /. (j + 1) = Z +* (y0 | (Seg (((len G) + 1) -' (j + 1)))) by A4;
(proj (modetrans (G,(((len G) + 1) -' j)))) . (h /. (j + 1)) = h2 . (((len G) + 1) -' j) by B3, Def1
.= Z . (((len G) + 1) -' j) by B8, C3, FUNCT_4:11
.= (proj (modetrans (G,(((len G) + 1) -' j)))) . (0. (product G)) by B3, A2, Def1 ;
hence ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. (j + 1)))) = (proj (modetrans (G,(((len G) + 1) -' j)))) . (y - (0. (product G))) by A7, B7, YTh9M
.= (proj (modetrans (G,(((len G) + 1) -' j)))) . y by RLVECT_1:13 ;
:: thesis: verum