let G be RealNormSpace-Sequence; :: thesis:
let S be RealNormSpace; :: thesis:
let f be PartFunc of (product G),S; :: thesis:
let x, y be Point of (product G); :: thesis:
set m = len G;
A1: the carrier of (product G) = product (carr G) by Th10;
reconsider Z0 = 0. (product G) as Element of product (carr G) by Th10;
reconsider y0 = y as Element of product (carr G) by Th10;
reconsider y1 = y as len G -element FinSequence ;
reconsider Z1 = 0. (product G) as len G -element FinSequence ;
len y1 = len G by CARD_1:def 7;
then A2: dom y1 = dom G by FINSEQ_3:29;
len Z1 = len G by CARD_1:def 7;
then A3: dom Z1 = dom G by FINSEQ_3:29;
defpred S₁[ Nat, set ] means $2 = Z0 +* (y0 | (Seg (((len G) + 1) -' $1)));
A4: for k being Nat st k in Seg ((len G) + 1) holds
ex x being Element of (product G) st S₁[k,x]

let k be Nat; :: thesis:
assume k in Seg ((len G) + 1) ; :: thesis:
Z0 +* (y0 | (Seg (((len G) + 1) -' k))) is Element of product (carr G) by CARD_3:79;
hence ex x being Element of (product G) st S₁[k,x] by A1; :: thesis:

end;

consider h being FinSequence of (product G) such that
A5: ( dom h = Seg ((len G) + 1) & ( for j being Nat st j in Seg ((len G) + 1) holds
S₁[j,h . j] ) ) from FINSEQ_1:sch 5(A4);

end;

deffunc H₁( Nat) -> Element of the carrier of S = f /. (x + (h /. $1));
consider z being FinSequence of S such that
A8: ( len z = (len G) + 1 & ( for j being Nat st j in dom z holds
z . j = H₁(j) ) ) from FINSEQ_2:sch 1();

end;

deffunc H₂( Nat) -> Element of the carrier of S = (z /. $1) - (z /. ($1 + 1));
consider g being FinSequence of S such that
A11: ( len g = len G & ( for j being Nat st j in dom g holds
g . j = H₂(j) ) ) from FINSEQ_2:sch 1();

end;

A14: ((len G) + 1) -' 1 = ((len G) + 1) - 1 by NAT_1:11, XREAL_1:233;
reconsider zz0 = 0 as Element of NAT ;
1 <= (len G) + 1 by NAT_1:11;
then A15: 1 in dom h by A5;
then h /. 1 = Z0 +* (y0 | (Seg (((len G) + 1) -' 1))) by A6
.= Z0 +* (y0 | (dom G)) by A14, FINSEQ_1:def 3
.= Z0 +* y0 by A2 ;
then A16: h /. 1 = y by A2, A3, FUNCT_4:19;
A17: ((len G) + 1) -' (len z) = ((len G) + 1) - (len z) by A8, XREAL_1:233;
( 1 <= len z & len z <= (len G) + 1 ) by A8, NAT_1:14;
then A18: len z in dom h by A5;
then A19: h /. (len z) = Z0 +* (y0 | (Seg 0)) by A6, A17, A8
.= 0. (product G) ;
A20: dom h = dom z by A5, A8, FINSEQ_1:def 3;
then A21: z /. 1 = f /. (x + y) by A9, A16, A15;
z /. (len z) = f /. (x + (h /. (len z))) by A9, A20, A18;
then A22: z /. (len z) = f /. x by A19, RLVECT_1:def 4;
take h ; :: thesis:
take g ; :: thesis:
take Z0 ; :: thesis:
take y0 ; :: thesis:

end;

end;

hence ( y0 = y & Z0 = 0. (product G) & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds
h /. i = Z0 +* (y0 | (Seg (((len G) + 1) -' i))) ) & ( for i being Nat st i in dom g holds
g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) ) & ( for i being Nat
for hi being Point of (product G) st i in dom h & h /. i = hi holds
||.hi.|| <= ||.y.|| ) & (f /. (x + y)) - (f /. x) = Sum g ) by A6, A21, A22, A23, A8, A12, Th42, A5, A11, FINSEQ_1:def 3; :: thesis: