let G be RealNormSpace-Sequence; :: thesis: for S being 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 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;
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 S1[ 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 S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg ((len G) + 1) implies ex x being Element of (product G) st S1[k,x] )
assume k in Seg ((len G) + 1) ; :: thesis: ex x being Element of (product G) st S1[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 S1[k,x] by A1; :: thesis: verum
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
S1[j,h . j] ) ) from FINSEQ_1:sch 5(A4);
A6: now :: thesis: for j being Nat st j in dom h holds
h /. j = Z0 +* (y0 | (Seg (((len G) + 1) -' j)))
let j be Nat; :: thesis: ( j in dom h implies h /. j = Z0 +* (y0 | (Seg (((len G) + 1) -' j))) )
assume A7: 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 A7, A5; :: thesis: verum
end;
deffunc H1( 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 = H1(j) ) ) from FINSEQ_2:sch 1();
A9: now :: thesis: for j being Nat st j in dom z holds
z /. j = f /. (x + (h /. j))
let j be Nat; :: thesis: ( j in dom z implies z /. j = f /. (x + (h /. j)) )
assume A10: 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 A10, A8; :: thesis: verum
end;
deffunc H2( 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 = H2(j) ) ) from FINSEQ_2:sch 1();
A12: now :: thesis: for j being Nat st j in dom g holds
g /. j = (z /. j) - (z /. (j + 1))
let j be Nat; :: thesis: ( j in dom g implies g /. j = (z /. j) - (z /. (j + 1)) )
assume A13: 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 A13, A11; :: thesis: verum
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: 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 )
A23: now :: thesis: for i being Nat st i in dom g holds
g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1))))
let i be Nat; :: thesis: ( i in dom g implies g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) )
assume A24: i in dom g ; :: thesis: g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1))))
then A25: i in Seg (len G) by A11, FINSEQ_1:def 3;
then ( 1 <= i & i <= len G ) by FINSEQ_1:1;
then A26: i + 1 <= (len G) + 1 by XREAL_1:6;
Seg (len G) c= Seg ((len G) + 1) by NAT_1:11, FINSEQ_1:5;
then A27: z /. i = f /. (x + (h /. i)) by A9, A5, A25, A20;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg ((len G) + 1) by A26;
then i + 1 in dom z by A8, FINSEQ_1:def 3;
then z /. (i + 1) = f /. (x + (h /. (i + 1))) by A9;
hence g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) by A12, A24, A27; :: thesis: verum
end;
now :: thesis: for i being Nat
for hi being Element of (product G) st i in dom h & h /. i = hi holds
||.hi.|| <= ||.y.||
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 A28: ( i in dom h & h /. i = hi ) ; :: thesis: ||.hi.|| <= ||.y.||
then h /. i = Z0 +* (y0 | (Seg (((len G) + 1) -' i))) by A6;
hence ||.hi.|| <= ||.y.|| by Th44, A28; :: 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 A6, A21, A22, A23, A8, A12, Th42, A5, A11, FINSEQ_1:def 3; :: thesis: verum