let G be 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 A6: 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 A7: 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 A8: In ((((len G) + 1) -' j),(dom G)) = ((len G) + 1) -' j by SUBSET_1:def 8;
set xh = x + (h /. (j + 1));
reconsider x1 = x, y1 = y as Element of product (carr G) by Th10;
reconsider xy = x + y as Element of product (carr G) by Th10;
x + (h /. (j + 1)) is Element of product (carr G) by Th10;
then consider g being Function such that
A9: ( x + (h /. (j + 1)) = g & dom g = dom (carr G) & ( for y being object st y in dom (carr G) holds
g . y in (carr G) . y ) ) by CARD_3:def 5;
A10: dom (x + (h /. (j + 1))) = dom G by A9, Lm1;
(proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y) = xy . (((len G) + 1) -' j) by A8, Def3;
then A11: (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y)) = (x + (h /. (j + 1))) +* ((In ((((len G) + 1) -' j),(dom G))),(xy . (((len G) + 1) -' j))) by Def4
.= (x + (h /. (j + 1))) +* ((In ((((len G) + 1) -' j),(dom G))) .--> (xy . (((len G) + 1) -' j))) by A10, FUNCT_7:def 3
.= (x + (h /. (j + 1))) +* ({(((len G) + 1) -' j)} --> (xy . (((len G) + 1) -' j))) by A8, FUNCOP_1:def 9 ;
reconsider F1 = x + (h /. j) as len G -element FinSequence ;
reconsider F2 = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y)) as len G -element FinSequence ;
reconsider h1 = h /. j as Element of product (carr G) by Th10;
reconsider xh1 = x + (h /. j) as Element of product (carr G) by Th10;
reconsider h2 = h /. (j + 1) as Element of product (carr G) by Th10;
A12: ( 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 A13: ( 1 <= k & k <= len F1 ) ; :: thesis:
then A14: k in Seg (len F1) ;
then reconsider k1 = k as Element of dom G by CARD_1:def 7, FINSEQ_1:def 3;
(proj k1) . xh1 = ((proj k1) . x) + ((proj k1) . (h /. j)) by Th35;
then A15: F1 . k = ((proj k1) . x) + ((proj k1) . (h /. j)) by Def3;
y0 is Element of the carrier of (product G) by Th10;
then A16: dom y0 = Seg (len G) by FINSEQ_1:89;
A17: (proj k1) . (h /. j) = h1 . k by Def3;
A18: dom (y0 | (Seg (((len G) + 1) -' j))) = (dom y0) /\ (Seg (((len G) + 1) -' j)) by RELAT_1:61;
A19: the carrier of (product G) = product (carr G) by Th10;

per cases ;

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

then not k in dom (y0 | (Seg (((len G) + 1) -' j))) by A18, XBOOLE_0:def 4;
then (proj k1) . (h /. j) = Z . k by A17, A6, FUNCT_4:11;
then A21: (proj k1) . (h /. j) = (proj k1) . (0. (product G)) by A2, Def3;
( not 1 <= k or not k <= ((len G) + 1) -' j ) by A20;
then not k in dom ({(((len G) + 1) -' j)} --> (xy . (((len G) + 1) -' j))) by A13, 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 A22: F2 . k = (proj k1) . (x + (h /. (j + 1))) by A19, A11, Def3;
A23: (proj k1) . (h /. (j + 1)) = h2 . k by Def3;
((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 A20;
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, A23, A7, Def3;
hence F1 . k = F2 . k by A21, A15, A22, Th35; :: thesis:

end;

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

then A25: k in dom (y0 | (Seg (((len G) + 1) -' j))) by A18, A14, A16, A12, XBOOLE_0:def 4;
then (proj k1) . (h /. j) = (y0 | (Seg (((len G) + 1) -' j))) . k by A17, A6, FUNCT_4:13;
then (proj k1) . (h /. j) = y0 . k by A25, FUNCT_1:47;
then A26: (proj k1) . (h /. j) = (proj k1) . y by A1, Def3;
then A27: F1 . k = (proj k1) . (x + y) by A15, Th35;

per cases ;

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

A29: k in {k} by TARSKI:def 1;
then k in dom ({k} --> (xy . k)) ;
then ((x + (h /. (j + 1))) +* ({k} --> (xy . k))) . k1 = ({k} --> (xy . k)) . k by FUNCT_4:13;
then F2 . k = xy . k by A11, A29, A28, FUNCOP_1:7;
hence F1 . k = F2 . k by A27, Def3; :: thesis:

end;

suppose A30: 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 A11, FUNCT_4:11;
then A31: F2 . k = (proj k1) . (x + (h /. (j + 1))) by A19, Def3;
k <= ((len G) + 1) -' j by A24, FINSEQ_1:1;
then k < ((len G) + 1) -' j by A30, 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 A13;
then A32: k in dom (y0 | (Seg (((len G) + 1) -' (j + 1)))) by A14, A16, A12, RELAT_1:57;
(proj k1) . (h /. (j + 1)) = h2 . k by Def3;
then (proj k1) . (h /. (j + 1)) = (y0 | (Seg (((len G) + 1) -' (j + 1)))) . k1 by A7, A32, FUNCT_4:13;
then (proj k1) . (h /. (j + 1)) = y0 . k by A32, FUNCT_1:47;
then (proj k1) . (h /. (j + 1)) = (proj k1) . y by A1, Def3;
hence F1 . k = F2 . k by A26, A15, A31, Th35; :: thesis:

end;

hence x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y)) by A12; :: thesis: