let G be non-trivial RealNormSpace-Sequence; :: thesis:
let h be FinSequence of (product G); :: thesis:
let y, x be Point of (product G); :: thesis:
let y0, Z be Element of product (carr G); :: thesis:
let j be Element of NAT ; :: thesis:
assume that
A1: y = y0 and
A2: Z = 0. (product G) and
A3: len h = (len G) + 1 and
A4: ( 1 <= j & j <= len G ) and
A5: for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ; :: thesis:
len G <= len h by A3, NAT_1:11;
then j <= len h by A4, XXREAL_0:2;
then j in Seg (len h) by A4;
then j in dom h by FINSEQ_1:def 3;
then X1: h /. j = Z +* (y0 | (Seg (((len G) + 1) -' j))) by A5;
( 1 <= j + 1 & j + 1 <= len h ) by A3, A4, 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 X2: h /. (j + 1) = Z +* (y0 | (Seg (((len G) + 1) -' (j + 1)))) by A5;
j in Seg (len G) by A4;
then ((len G) -' j) + 1 in Seg (len G) by NAT_2:6;
then ((len G) + 1) -' j in Seg (len G) by A4, NAT_D:38;
then ((len G) + 1) -' j in dom G by FINSEQ_1:def 3;
then A6: modetrans (G,(((len G) + 1) -' j)) = ((len G) + 1) -' j by Defmode;
set xh = x + (h /. (j + 1));
reconsider x1 = x, y1 = y as Element of product (carr G) by LM001;
reconsider xy = x + y as Element of product (carr G) by LM001;
x + (h /. (j + 1)) is Element of product (carr G) by LM001;
then consider g being Function such that
H2: ( x + (h /. (j + 1)) = g & dom g = dom (carr G) & ( for y being set st y in dom (carr G) holds
g . y in (carr G) . y ) ) by CARD_3:def 5;
PO: dom (x + (h /. (j + 1))) = dom G by H2, ZE;
(proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y) = xy . (((len G) + 1) -' j) by A6, Def1;
then A8: (reproj ((modetrans (G,(((len G) + 1) -' j))),(x + (h /. (j + 1))))) . ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) = (x + (h /. (j + 1))) +* ((modetrans (G,(((len G) + 1) -' j))),(xy . (((len G) + 1) -' j))) by Def5
.= (x + (h /. (j + 1))) +* ((modetrans (G,(((len G) + 1) -' j))) .--> (xy . (((len G) + 1) -' j))) by FUNCT_7:def 3, PO
.= (x + (h /. (j + 1))) +* ({(((len G) + 1) -' j)} --> (xy . (((len G) + 1) -' j))) by A6, FUNCOP_1:def 9 ;
reconsider F1 = x + (h /. j) as len G -element FinSequence ;
reconsider F2 = (reproj ((modetrans (G,(((len G) + 1) -' j))),(x + (h /. (j + 1))))) . ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) as len G -element FinSequence ;
reconsider h1 = h /. j as Element of product (carr G) by LM001;
reconsider xh1 = x + (h /. j) as Element of product (carr G) by LM001;
reconsider h2 = h /. (j + 1) as Element of product (carr G) by LM001;
A9: ( len F1 = len G & len F2 = len G ) by CARD_1:def 7;
for k being Nat st 1 <= k & k <= len F1 holds
F1 . k = F2 . k

proof

let k be Nat; :: thesis:
assume W1: ( 1 <= k & k <= len F1 ) ; :: thesis:
then BB: k in Seg (len F1) by FINSEQ_1:1;
then reconsider k1 = k as Element of dom G by A9, FINSEQ_1:def 3;
(proj k1) . xh1 = ((proj k1) . x) + ((proj k1) . (h /. j)) by YTh9;
then B2: F1 . k = ((proj k1) . x) + ((proj k1) . (h /. j)) by Def1;
y0 is Element of the carrier of (product G) by LM001;
then C0: dom y0 = Seg (len G) by FINSEQ_1:89;
G0: (proj k1) . (h /. j) = h1 . k by Def1;
G1: dom (y0 | (Seg (((len G) + 1) -' j))) = (dom y0) /\ (Seg (((len G) + 1) -' j)) by RELAT_1:61;
ZZ: the carrier of (product G) = product (carr G) by LM001;

per cases ;

suppose H1: not k in Seg (((len G) + 1) -' j) ; :: thesis:

then not k in dom (y0 | (Seg (((len G) + 1) -' j))) by G1, XBOOLE_0:def 4;
then (proj k1) . (h /. j) = Z . k by G0, X1, FUNCT_4:11;
then H4: (proj k1) . (h /. j) = (proj k1) . (0. (product G)) by A2, Def1;
( not 1 <= k or not k <= ((len G) + 1) -' j ) by H1, FINSEQ_1:1;
then not k in dom ({(((len G) + 1) -' j)} --> (xy . (((len G) + 1) -' j))) by W1, TARSKI:def 1;
then ((x + (h /. (j + 1))) +* ({(((len G) + 1) -' j)} --> (xy . (((len G) + 1) -' j)))) . k1 = (x + (h /. (j + 1))) . k1 by FUNCT_4:11;
then H3: F2 . k = (proj k1) . (x + (h /. (j + 1))) by ZZ, A8, Def1;
H2: (proj k1) . (h /. (j + 1)) = h2 . k by Def1;
((len G) + 1) -' (j + 1) <= ((len G) + 1) -' j by NAT_1:11, NAT_D:41;
then Seg (((len G) + 1) -' (j + 1)) c= Seg (((len G) + 1) -' j) by FINSEQ_1:5;
then not k in Seg (((len G) + 1) -' (j + 1)) by H1;
then not k in (dom y0) /\ (Seg (((len G) + 1) -' (j + 1))) by XBOOLE_0:def 4;
then not k in dom (y0 | (Seg (((len G) + 1) -' (j + 1)))) by RELAT_1:61;
then (Z +* (y0 | (Seg (((len G) + 1) -' (j + 1))))) . k = Z . k by FUNCT_4:11;
then (proj k1) . (h /. (j + 1)) = (proj k1) . (0. (product G)) by A2, H2, X2, Def1;
hence F1 . k = F2 . k by H4, B2, H3, YTh9; :: thesis:

end;

suppose G7: k in Seg (((len G) + 1) -' j) ; :: thesis:

then G2: k in dom (y0 | (Seg (((len G) + 1) -' j))) by G1, BB, C0, A9, XBOOLE_0:def 4;
then (proj k1) . (h /. j) = (y0 | (Seg (((len G) + 1) -' j))) . k by G0, X1, FUNCT_4:13;
then (proj k1) . (h /. j) = y0 . k by G2, FUNCT_1:47;
then G5: (proj k1) . (h /. j) = (proj k1) . y by A1, Def1;
then H5: F1 . k = (proj k1) . (x + y) by B2, YTh9;

per cases ;

suppose G4: k = ((len G) + 1) -' j ; :: thesis:

G3: k in {k} by TARSKI:def 1;
then k in dom ({k} --> (xy . k)) by FUNCOP_1:13;
then ((x + (h /. (j + 1))) +* ({k} --> (xy . k))) . k1 = ({k} --> (xy . k)) . k by FUNCT_4:13;
then F2 . k = xy . k by A8, G3, G4, FUNCOP_1:7;
hence F1 . k = F2 . k by H5, Def1; :: thesis:

end;

suppose G8: k <> ((len G) + 1) -' j ; :: thesis:

then not k in dom ({(((len G) + 1) -' j)} --> (xy . (((len G) + 1) -' j))) by TARSKI:def 1;
then F2 . k = (x + (h /. (j + 1))) . k by A8, FUNCT_4:11;
then G6: F2 . k = (proj k1) . (x + (h /. (j + 1))) by ZZ, Def1;
k <= ((len G) + 1) -' j by G7, FINSEQ_1:1;
then k < ((len G) + 1) -' j by G8, XXREAL_0:1;
then k <= (((len G) + 1) -' j) -' 1 by NAT_D:49;
then k <= ((len G) + 1) -' (j + 1) by NAT_2:30;
then k in Seg (((len G) + 1) -' (j + 1)) by W1, FINSEQ_1:1;
then W2: k in dom (y0 | (Seg (((len G) + 1) -' (j + 1)))) by BB, C0, A9, RELAT_1:57;
(proj k1) . (h /. (j + 1)) = h2 . k by Def1;
then (proj k1) . (h /. (j + 1)) = (y0 | (Seg (((len G) + 1) -' (j + 1)))) . k1 by X2, W2, FUNCT_4:13;
then (proj k1) . (h /. (j + 1)) = y0 . k by W2, FUNCT_1:47;
then (proj k1) . (h /. (j + 1)) = (proj k1) . y by A1, Def1;
hence F1 . k = F2 . k by G5, B2, G6, YTh9; :: thesis:

end;

hence x + (h /. j) = (reproj ((modetrans (G,(((len G) + 1) -' j))),(x + (h /. (j + 1))))) . ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) by A9, FINSEQ_1:def 17; :: thesis: