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, Th54;
then (proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. j)) = (proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y) by Th46;
then A5: ((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 Th37;
(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 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)))) . (h /. j)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (h /. (j + 1))) by A5, Th37;
y0 is Element of the carrier of (product G) by Th10;
then A7: 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 A8: ((len G) + 1) -' j in Seg (len G) by A3, NAT_D:38;
A9: 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 A10: ((len G) + 1) -' j in dom (y0 | (Seg (((len G) + 1) -' j))) by A7, A8, RELAT_1:57;
((len G) + 1) -' j = (((len G) + 1) -' (j + 1)) + 1 by A9, NAT_2:7;
then A11: ((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 A12: not ((len G) + 1) -' j in dom (y0 | (Seg (((len G) + 1) -' (j + 1)))) by A11, FINSEQ_1:1;
reconsider h1 = h /. j as Element of product (carr G) by Th10;
reconsider h2 = h /. (j + 1) as Element of product (carr G) by Th10;
j in Seg (len h) by A3, A9;
then j in dom h by FINSEQ_1:def 3;
then A13: h /. j = Z +* (y0 | (Seg (((len G) + 1) -' j))) by A4;
((len G) + 1) -' j in dom G by A8, FINSEQ_1:def 3;
then A14: modetrans (G,(((len G) + 1) -' j)) = ((len G) + 1) -' j by Def5;
then A15: (proj (modetrans (G,(((len G) + 1) -' j)))) . (h /. j) = h1 . (((len G) + 1) -' j) by Def3
.= (y0 | (Seg (((len G) + 1) -' j))) . (((len G) + 1) -' j) by A10, A13, FUNCT_4:13
.= y0 . (((len G) + 1) -' j) by A10, FUNCT_1:47
.= (proj (modetrans (G,(((len G) + 1) -' j)))) . y by A1, A14, Def3 ;
( 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 A16: 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 A14, Def3
.= Z . (((len G) + 1) -' j) by A16, A12, FUNCT_4:11
.= (proj (modetrans (G,(((len G) + 1) -' j)))) . (0. (product G)) by A14, A2, Def3 ;
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 A6, A15, Th37
.= (proj (modetrans (G,(((len G) + 1) -' j)))) . y by RLVECT_1:13 ;
:: thesis: verum