let G be non-trivial RealNormSpace-Sequence; :: thesis: for S being non trivial RealNormSpace
for f being PartFunc of (product G),S
for x, y being Point of (product G) ex h being FinSequence of (product G) ex g being FinSequence of S ex Z, y0 being Element of product (carr G) st
( y0 = y & Z = 0. (product G) & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (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 )
let S be non trivial RealNormSpace; :: thesis: for f being PartFunc of (product G),S
for x, y being Point of (product G) ex h being FinSequence of (product G) ex g being FinSequence of S ex Z, y0 being Element of product (carr G) st
( y0 = y & Z = 0. (product G) & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (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 )
let f be PartFunc of (product G),S; :: thesis: for x, y being Point of (product G) ex h being FinSequence of (product G) ex g being FinSequence of S ex Z, y0 being Element of product (carr G) st
( y0 = y & Z = 0. (product G) & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (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 )
let x, y be Point of (product G); :: thesis: ex h being FinSequence of (product G) ex g being FinSequence of S ex Z, y0 being Element of product (carr G) st
( y0 = y & Z = 0. (product G) & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (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 )
set m = len G;
CG1: the carrier of (product G) = product (carr G) by LM001;
reconsider Z0 = 0. (product G) as Element of product (carr G) by LM001;
reconsider y0 = y as Element of product (carr G) by LM001;
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 B1: dom y1 = dom G by FINSEQ_3:29;
len Z1 = len G by CARD_1:def 7;
then B2: dom Z1 = dom G by FINSEQ_3:29;
defpred S₁[ Nat, set ] means $2 = Z0 +* (y0 | (Seg (((len G) + 1) -' $1)));
A2: for k being Nat st k in Seg ((len G) + 1) holds
ex x being Element of (product G) st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg ((len G) + 1) implies ex x being Element of (product G) st S₁[k,x] )
assume k in Seg ((len G) + 1) ; :: thesis: ex x being Element of (product G) st S₁[k,x]
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 CG1; :: thesis: verum

end;

consider h being FinSequence of (product G) such that
A6: ( 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(A2);

A7: now

let j be Nat; :: thesis: ( j in dom h implies h /. j = Z0 +* (y0 | (Seg (((len G) + 1) -' j))) )
assume A8: j in dom h ; :: thesis: h /. j = Z0 +* (y0 | (Seg (((len G) + 1) -' j)))
then h /. j = h . j by PARTFUN1:def 6;
hence h /. j = Z0 +* (y0 | (Seg (((len G) + 1) -' j))) by A8, A6; :: thesis: verum

end;

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

A10: now

let j be Nat; :: thesis: ( j in dom z implies z /. j = f /. (x + (h /. j)) )
assume A11: j in dom z ; :: thesis: z /. j = f /. (x + (h /. j))
then z /. j = z . j by PARTFUN1:def 6;
hence z /. j = f /. (x + (h /. j)) by A11, A9; :: thesis: verum

end;

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

A13: now

let j be Nat; :: thesis: ( j in dom g implies g /. j = (z /. j) - (z /. (j + 1)) )
assume A14: j in dom g ; :: thesis: g /. j = (z /. j) - (z /. (j + 1))
then g /. j = g . j by PARTFUN1:def 6;
hence g /. j = (z /. j) - (z /. (j + 1)) by A14, A12; :: thesis: verum

end;

A16: ((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 C2: 1 in dom h by A6;
then h /. 1 = Z0 +* (y0 | (Seg (((len G) + 1) -' 1))) by A7
.= Z0 +* (y0 | (dom G)) by A16, FINSEQ_1:def 3
.= Z0 +* y0 by B1, RELAT_1:69 ;
then A17: h /. 1 = y by B1, B2, FUNCT_4:19;
A19: ((len G) + 1) -' (len z) = ((len G) + 1) - (len z) by A9, XREAL_1:233;
( 1 <= len z & len z <= (len G) + 1 ) by A9, NAT_1:14;
then C3: len z in dom h by A6;
then A21: h /. (len z) = Z0 +* (y0 | (Seg 0)) by A7, A19, A9
.= 0. (product G) by FUNCT_4:21 ;
C1: dom h = dom z by A6, A9, FINSEQ_1:def 3;
then A22: z /. 1 = f /. (x + y) by A10, A17, C2;
z /. (len z) = f /. (x + (h /. (len z))) by A10, C1, C3;
then A23: z /. (len z) = f /. x by A21, RLVECT_1:def 4;
take h ; :: thesis: ex g being FinSequence of S ex Z, y0 being Element of product (carr G) st
( y0 = y & Z = 0. (product G) & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (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 )
take g ; :: thesis: ex Z, y0 being Element of product (carr G) st
( y0 = y & Z = 0. (product G) & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (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 )
take Z0 ; :: thesis: ex y0 being Element of product (carr G) st
( 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 )
take y0 ; :: thesis: ( 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 )

A24: now

let i be Nat; :: thesis: ( i in dom g implies g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) )
assume A25: i in dom g ; :: thesis: g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1))))
then A26: i in Seg (len G) by A12, FINSEQ_1:def 3;
then ( 1 <= i & i <= len G ) by FINSEQ_1:1;
then A29: i + 1 <= (len G) + 1 by XREAL_1:6;
len G <= (len G) + 1 by NAT_1:11;
then Seg (len G) c= Seg ((len G) + 1) by FINSEQ_1:5;
then A28: z /. i = f /. (x + (h /. i)) by A10, A6, A26, C1;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg ((len G) + 1) by A29;
then i + 1 in dom z by A9, FINSEQ_1:def 3;
then z /. (i + 1) = f /. (x + (h /. (i + 1))) by A10;
hence g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) by A13, A25, A28; :: thesis: verum

end;

now

let i be Nat; :: thesis: for hi being Element of (product G) st i in dom h & h /. i = hi holds
||.hi.|| <= ||.y.||
let hi be Element of (product G); :: thesis: ( i in dom h & h /. i = hi implies ||.hi.|| <= ||.y.|| )
assume ASD: ( i in dom h & h /. i = hi ) ; :: thesis: ||.hi.|| <= ||.y.||
then h /. i = Z0 +* (y0 | (Seg (((len G) + 1) -' i))) by A7;
hence ||.hi.|| <= ||.y.|| by LMPRT3, ASD; :: thesis: verum

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 A7, A22, A23, A24, A9, A13, Th26, A6, A12, FINSEQ_1:def 3; :: thesis: verum