let m, n be non zero Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for x, y being Element of REAL m ex h being FinSequence of REAL m ex g being FinSequence of REAL n st
( len h = m + 1 & len g = m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) & ( 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 Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.| ) & (f /. (x + y)) - (f /. x) = Sum g )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for x, y being Element of REAL m ex h being FinSequence of REAL m ex g being FinSequence of REAL n st
( len h = m + 1 & len g = m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) & ( 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 Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.| ) & (f /. (x + y)) - (f /. x) = Sum g )
let x, y be Element of REAL m; :: thesis: ex h being FinSequence of REAL m ex g being FinSequence of REAL n st
( len h = m + 1 & len g = m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) & ( 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 Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.| ) & (f /. (x + y)) - (f /. x) = Sum g )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A1: len y = mm by FINSEQ_2:133;
defpred S₁[ Nat, set ] means $2 = (y | ((m + 1) -' $1)) ^ (0* ($1 -' 1));
A2: for k being Nat st k in Seg (m + 1) holds
ex x being Element of REAL m st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (m + 1) implies ex x being Element of REAL m st S₁[k,x] )
assume k in Seg (m + 1) ; :: thesis: ex x being Element of REAL m st S₁[k,x]
then A3: ( 1 <= k & k <= m + 1 ) by FINSEQ_1:1;
then ( k - 1 >= 0 & (m + 1) - k >= 0 ) by XREAL_1:48;
then A4: ( (m + 1) -' k = (m + 1) - k & k -' 1 = k - 1 ) by XREAL_0:def 2;
set l1 = (m + 1) -' k;
set l2 = k -' 1;
m + 1 <= m + k by A3, XREAL_1:6;
then (m + 1) -' k <= len y by A1, A4, XREAL_1:20;
then A5: len (y | ((m + 1) -' k)) = (m + 1) -' k by FINSEQ_1:59;
len (0* (k -' 1)) = k -' 1 by FINSEQ_2:132;
then len ((y | ((m + 1) -' k)) ^ (0* (k -' 1))) = ((m + 1) -' k) + (k -' 1) by A5, FINSEQ_1:22;
then (y | ((m + 1) -' k)) ^ (0* (k -' 1)) is Element of (((m + 1) -' k) + (k -' 1)) -tuples_on REAL by FINSEQ_2:133;
hence ex x being Element of REAL m st S₁[k,x] by A4; :: thesis: verum

end;

consider h being FinSequence of REAL m such that
A6: ( dom h = Seg (m + 1) & ( for j being Nat st j in Seg (m + 1) holds
S₁[j,h . j] ) ) from FINSEQ_1:sch 5(A2);

A7: now :: thesis: for j being Nat st j in dom h holds
h /. j = (y | ((m + 1) -' j)) ^ (0* (j -' 1))

let j be Nat; :: thesis: ( j in dom h implies h /. j = (y | ((m + 1) -' j)) ^ (0* (j -' 1)) )
assume A8: j in dom h ; :: thesis: h /. j = (y | ((m + 1) -' j)) ^ (0* (j -' 1))
then h /. j = h . j by PARTFUN1:def 6;
hence h /. j = (y | ((m + 1) -' j)) ^ (0* (j -' 1)) by A8, A6; :: thesis: verum

end;

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

A10: 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 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 REAL n = (z /. $1) - (z /. ($1 + 1));
consider g being FinSequence of REAL n such that
A12: ( len g = m & ( for j being Nat st j in dom g holds
g . j = H₂(j) ) ) from FINSEQ_2:sch 1();

A13: 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 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;

A15: 1 <= m + 1 by NAT_1:11;
A16: (m + 1) -' 1 = (m + 1) - 1 by NAT_1:11, XREAL_1:233;
1 in dom h by A6, A15;
then h /. 1 = (y | ((m + 1) -' 1)) ^ (0* (1 -' 1)) by A7;
then h /. 1 = (y | m) ^ (0* 0) by A16, XREAL_1:232;
then h /. 1 = y ^ (0* 0) by A1, FINSEQ_1:58;
then A17: h /. 1 = y by FINSEQ_1:34;
A18: ( 1 <= len z & len z <= m + 1 ) by A9, NAT_1:14;
A19: (m + 1) -' (len z) = (m + 1) - (len z) by A9, XREAL_1:233;
A20: (len z) -' 1 = (len z) - 1 by A9, NAT_1:14, XREAL_1:233;
len z in dom h by A6, A18;
then h /. (len z) = (y | 0) ^ (0* ((len z) -' 1)) by A7, A19, A9;
then A21: h /. (len z) = 0* m by A20, A9, FINSEQ_1:34;
1 <= m + 1 by NAT_1:11;
then 1 in Seg (m + 1) ;
then 1 in dom z by A9, FINSEQ_1:def 3;
then A22: z /. 1 = f /. (x + y) by A10, A17;
len z in Seg (m + 1) by A9, FINSEQ_1:4;
then len z in dom z by A9, FINSEQ_1:def 3;
then z /. (len z) = f /. (x + (h /. (len z))) by A10;
then A23: z /. (len z) = f /. x by A21, EUCLID_4:1;
take h ; :: thesis: ex g being FinSequence of REAL n st
( len h = m + 1 & len g = m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) & ( 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 Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.| ) & (f /. (x + y)) - (f /. x) = Sum g )
take g ; :: thesis: ( len h = m + 1 & len g = m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) & ( 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 Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.| ) & (f /. (x + y)) - (f /. x) = Sum g )
m + 1 in NAT by ORDINAL1:def 12;
hence ( len h = m + 1 & len g = m ) by A6, A12, FINSEQ_1:def 3; :: thesis: ( ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) & ( 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 Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.| ) & (f /. (x + y)) - (f /. x) = Sum g )

A24: 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 A25: i in dom g ; :: thesis: g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1))))
then A26: i in Seg m by A12, FINSEQ_1:def 3;
m <= m + 1 by NAT_1:11;
then A27: Seg m c= Seg (m + 1) by FINSEQ_1:5;
dom h = dom z by A6, A9, FINSEQ_1:def 3;
then A28: z /. i = f /. (x + (h /. i)) by A10, A27, A6, A26;
i in Seg m by A12, A25, FINSEQ_1:def 3;
then ( 1 <= i & i <= m ) by FINSEQ_1:1;
then A29: i + 1 <= m + 1 by XREAL_1:6;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (m + 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;

for i being Nat
for hi being Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.|

proof

let i be Nat; :: thesis: for hi being Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.|
let hi be Element of REAL m; :: thesis: ( i in dom h & h /. i = hi implies |.hi.| <= |.y.| )
assume ( i in dom h & h /. i = hi ) ; :: thesis: |.hi.| <= |.y.|
then A30: hi = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) by A7;
A31: for j being Nat st j in Seg m holds
(sqr hi) . j <= (sqr y) . j

proof

let j be Nat; :: thesis: ( j in Seg m implies (sqr hi) . j <= (sqr y) . j )
assume A32: j in Seg m ; :: thesis: (sqr hi) . j <= (sqr y) . j
len hi = m by CARD_1:def 7;
then A33: j in dom ((y | ((m + 1) -' i)) ^ (0* (i -' 1))) by A32, A30, FINSEQ_1:def 3;

per cases ( j in dom (y | ((m + 1) -' i)) or ex k being Nat st
( k in dom (0* (i -' 1)) & j = (len (y | ((m + 1) -' i))) + k ) ) by A33, FINSEQ_1:25;

suppose A34: j in dom (y | ((m + 1) -' i)) ; :: thesis: (sqr hi) . j <= (sqr y) . j

then j in Seg (len (y | ((m + 1) -' i))) by FINSEQ_1:def 3;
then A35: j <= len (y | ((m + 1) -' i)) by FINSEQ_1:1;
A36: len (y | ((m + 1) -' i)) <= (m + 1) -' i by FINSEQ_5:17;
(sqr hi) . j = (sqrreal * hi) . j by RVSUM_1:def 8
.= sqrreal . (((y | ((m + 1) -' i)) ^ (0* (i -' 1))) . j) by A30, A33, FUNCT_1:13
.= sqrreal . ((y | ((m + 1) -' i)) . j) by A34, FINSEQ_1:def 7
.= sqrreal . (y . j) by A36, A35, FINSEQ_3:112, XXREAL_0:2
.= (y . j) ^2 by RVSUM_1:def 2
.= (sqr y) . j by VALUED_1:11 ;
hence (sqr hi) . j <= (sqr y) . j ; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom (0* (i -' 1)) & j = (len (y | ((m + 1) -' i))) + k ) ; :: thesis: (sqr hi) . j <= (sqr y) . j

then consider k being Nat such that
A37: ( k in dom (0* (i -' 1)) & j = (len (y | ((m + 1) -' i))) + k ) ;
A38: (sqr hi) . j = (sqrreal * hi) . j by RVSUM_1:def 8
.= sqrreal . (((y | ((m + 1) -' i)) ^ (0* (i -' 1))) . j) by A30, A33, FUNCT_1:13
.= sqrreal . ((0* (i -' 1)) . k) by A37, FINSEQ_1:def 7
.= ((0* (i -' 1)) . k) ^2 by RVSUM_1:def 2
.= 0 ;
(sqr y) . j = (y . j) ^2 by VALUED_1:11
.= (y . j) * (y . j) ;
hence (sqr hi) . j <= (sqr y) . j by A38, XREAL_1:63; :: thesis: verum

end;

end;

end;

0 <= Sum (sqr hi) by RVSUM_1:86;
hence |.hi.| <= |.y.| by A31, RVSUM_1:82, SQUARE_1:26; :: thesis: verum

end;

hence ( ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) & ( 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 Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.| ) & (f /. (x + y)) - (f /. x) = Sum g ) by A7, A22, A23, A24, A9, A12, A13, Th26; :: thesis: verum