let X be RealNormSpace-Sequence; :: thesis:
let Y be RealNormSpace; :: thesis:
let f be MultilinearOperator of X,Y; :: thesis:
let K be Real; :: thesis:
assume that
A1: 0 <= K and
A2: for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ; :: thesis:
A3: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
let v0 be Point of (product X); :: thesis:
consider g being Function such that
A4: ( v0 = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds
g . i in (carr X) . i ) ) by A3, CARD_3:def 5;
dom g = Seg (len (carr X)) by A4, FINSEQ_1:def 3;
then reconsider Cv0 = v0 as FinSequence by A4, FINSEQ_1:def 2;
set L = ||.v0.|| + 3;
set M = (||.v0.|| + 3) |^ (len X);
take (||.v0.|| + 3) |^ (len X) ; :: thesis:
thus 0 <= (||.v0.|| + 3) |^ (len X) by POWER:3; :: thesis:
defpred S₁[ Nat] means for v0, v1 being Point of (product X)
for Cv0, Cv1 being FinSequence st ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & $1 <= len X & Cv1 | ((len X) -' $1) = Cv0 | ((len X) -' $1) holds
ex F being FinSequence of REAL st
( dom F = Seg $1 & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( for n being Nat st n in Seg $1 holds
ex i being Element of dom X st
( i = ((len X) -' $1) + n & F . n = ||.((v1 - v0) . i).|| ) ) );
A6: S₁[ 0 ]

proof

let v0, v1 be Point of (product X); :: thesis:
let Cv0, Cv1 be FinSequence; :: thesis:
assume A7: ( ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & 0 <= len X & Cv1 | ((len X) -' 0) = Cv0 | ((len X) -' 0) ) ; :: thesis:
A8: (len X) -' 0 = ((len X) + 0) -' 0
.= len X by NAT_D:34 ;
reconsider F = <*> REAL as FinSequence of REAL ;
take F ; :: thesis:
thus dom F = Seg 0 ; :: thesis:
consider g being Function such that
A9: ( v0 = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds
g . i in (carr X) . i ) ) by A3, CARD_3:def 5;
A10: dom g = Seg (len (carr X)) by A9, FINSEQ_1:def 3;
then reconsider Cv0 = v0 as FinSequence by A9, FINSEQ_1:def 2;
A11: len Cv0 = len (carr X) by A9, A10, FINSEQ_1:def 3
.= len X by PRVECT_1:def 11 ;
consider g being Function such that
A12: ( v1 = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds
g . i in (carr X) . i ) ) by A3, CARD_3:def 5;
dom Cv1 = Seg (len (carr X)) by A7, A12, FINSEQ_1:def 3;
then A14: len Cv1 = len (carr X) by FINSEQ_1:def 3
.= len X by PRVECT_1:def 11 ;
Cv1 = Cv0 | (len X) by A7, A8, A14, FINSEQ_1:58
.= Cv0 by A11, FINSEQ_1:58 ;
then (f /. v1) - (f /. v0) = 0. Y by A7, RLVECT_1:15;
hence ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) by RVSUM_1:72; :: thesis:
thus for n being Nat st n in Seg 0 holds
ex i being Element of dom X st
( i = ((len X) -' 0) + n & F . n = ||.((v1 - v0) . i).|| ) ; :: thesis:

end;

A16: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A17: S₁[k] ; :: thesis:
let v0, v1 be Point of (product X); :: thesis:
let Cv0, Cv1 be FinSequence; :: thesis:
assume A18: ( ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & k + 1 <= len X & Cv1 | ((len X) -' (k + 1)) = Cv0 | ((len X) -' (k + 1)) ) ; :: thesis:
consider g being Function such that
A19: ( v0 = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds
g . i in (carr X) . i ) ) by A3, CARD_3:def 5;
dom g = Seg (len (carr X)) by A19, FINSEQ_1:def 3;
then reconsider Cv0 = v0 as FinSequence by A19, FINSEQ_1:def 2;
dom Cv0 = Seg (len (carr X)) by A19, FINSEQ_1:def 3;
then A21: len Cv0 = len (carr X) by FINSEQ_1:def 3
.= len X by PRVECT_1:def 11 ;
then A22: dom Cv0 = Seg (len X) by FINSEQ_1:def 3
.= dom X by FINSEQ_1:def 3 ;
consider g1 being Function such that
A23: ( v1 = g1 & dom g1 = dom (carr X) & ( for i being object st i in dom (carr X) holds
g1 . i in (carr X) . i ) ) by A3, CARD_3:def 5;
dom g1 = Seg (len (carr X)) by A23, FINSEQ_1:def 3;
then reconsider Cv1 = v1 as FinSequence by A23, FINSEQ_1:def 2;
1 <= 1 + k by NAT_1:11;
then 1 <= len X by A18, XXREAL_0:2;
then len X in Seg (len X) ;
then reconsider i = len X as Element of dom X by FINSEQ_1:def 3;

per cases ;

suppose A25: k = 0 ; :: thesis:

then A26: (len X) -' (k + 1) = (len X) - 1 by A18, XREAL_0:def 2;
for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j

proof

let j be Element of dom X; :: thesis:
j in dom X ;
then j in Seg (len X) by FINSEQ_1:def 3;
then A27: ( 1 <= j & j <= len X ) by FINSEQ_1:1;
assume i <> j ; :: thesis:
then j < len X by A27, XXREAL_0:1;
then j + 1 <= len X by NAT_1:13;
then (j + 1) - 1 <= (len X) - 1 by XREAL_1:9;
then A28: j in Seg ((len X) -' (k + 1)) by A26, A27;
thus Cv1 . j = (Cv0 | ((len X) -' (k + 1))) . j by A18, A28, FUNCT_1:49
.= Cv0 . j by A28, FUNCT_1:49 ; :: thesis:

end;

then A29: ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| by A1, A2, A18, LM02;
set F = <*||.((v1 - v0) . i).||*>;
rng <*||.((v1 - v0) . i).||*> c= REAL ;
then reconsider F = <*||.((v1 - v0) . i).||*> as FinSequence of REAL by FINSEQ_1:def 4;
take F ; :: thesis:
thus dom F = Seg (len F) by FINSEQ_1:def 3
.= Seg (k + 1) by A25, FINSEQ_1:40 ; :: thesis:
A31: ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * (Sum F) by A29, RVSUM_1:73;
(||.v0.|| + 1) + 0 <= (||.v0.|| + 1) + 2 by XREAL_1:7;
then A32: (||.v0.|| + 1) |^ (len X) <= (||.v0.|| + 3) |^ (len X) by PREPOWER:9;
0 <= Sum F by RVSUM_1:73;
then ((||.v0.|| + 1) |^ (len X)) * (K * (Sum F)) <= ((||.v0.|| + 3) |^ (len X)) * (K * (Sum F)) by A1, A32, XREAL_1:64;
hence ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) by A31, XXREAL_0:2; :: thesis:
thus for n being Nat st n in Seg (k + 1) holds
ex j being Element of dom X st
( j = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . j).|| ) :: thesis:

proof

let n be Nat; :: thesis:
assume A33: n in Seg (k + 1) ; :: thesis:
then A34: ((len X) -' (k + 1)) + n = ((len X) - 1) + 1 by A25, A26, FINSEQ_1:2, TARSKI:def 1
.= i ;
take i ; :: thesis:
n = 1 by A25, A33, FINSEQ_1:2, TARSKI:def 1;
hence ( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| ) by A34, FINSEQ_1:40; :: thesis:

end;

suppose k <> 0 ; :: thesis:

A35: (k + 1) - k <= (len X) - k by A18, XREAL_1:13;
A36: (len X) - k <= (len X) - 0 by XREAL_1:13;
(len X) - k in NAT by A35, INT_1:3;
then (len X) - k in Seg (len X) by A35, A36;
then reconsider k1 = (len X) - k as Element of dom X by FINSEQ_1:def 3;
Cv0 . k1 = v0 . k1 ;
then reconsider Cv0k1 = Cv0 . k1 as Point of (X . k1) ;
k <= k + 1 by NAT_1:11;
then A38: k <= len X by A18, XXREAL_0:2;
reconsider v2 = (reproj (k1,v1)) . Cv0k1 as Point of (product X) ;
consider g being Function such that
A39: ( v2 = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds
g . i in (carr X) . i ) ) by A3, CARD_3:def 5;
A40: dom g = Seg (len (carr X)) by A39, FINSEQ_1:def 3;
then reconsider Cv2 = v2 as FinSequence by A39, FINSEQ_1:def 2;
A41: len Cv2 = len (carr X) by A39, A40, FINSEQ_1:def 3
.= len X by PRVECT_1:def 11 ;
reconsider w12 = v1 - v2 as Element of product (carr X) by A3;
reconsider w02 = v2 - v0 as Element of product (carr X) by A3;
reconsider w10 = v1 - v0 as Element of product (carr X) by A3;
||.(v2 - v0).|| <= ||.(v1 - v0).||

proof

A42: ||.(v2 - v0).|| = |.(normsequence (X,w02)).| by A3, PRVECT_2:def 12;
A43: ||.(v1 - v0).|| = |.(normsequence (X,w10)).| by A3, PRVECT_2:def 12;
A44: 0 <= Sum (sqr (normsequence (X,w02))) by RVSUM_1:86;
for j being Nat st j in Seg (len X) holds
(sqr (normsequence (X,w02))) . j <= (sqr (normsequence (X,w10))) . j

proof

let j be Nat; :: thesis:
assume A45: j in Seg (len X) ; :: thesis:
reconsider i = j as Element of dom X by A45, FINSEQ_1:def 3;
A46: (sqr (normsequence (X,w02))) . j = ((normsequence (X,w02)) . j) ^2 by VALUED_1:11
.= ||.((v2 - v0) . i).|| ^2 by PRVECT_2:def 11 ;
A47: (sqr (normsequence (X,w10))) . j = ((normsequence (X,w10)) . j) ^2 by VALUED_1:11
.= ||.((v1 - v0) . i).|| ^2 by PRVECT_2:def 11 ;
A48: (v2 - v0) . i = (v2 . i) - (v0 . i) by LOPBAN10:26;
A49: (v1 - v0) . i = (v1 . i) - (v0 . i) by LOPBAN10:26;
||.((v2 - v0) . i).|| <= ||.((v1 - v0) . i).||

proof

per cases ;

suppose A50: i = k1 ; :: thesis:

v2 . i = v0 . i by A50, LOPBAN10:15;
then (v2 . i) - (v0 . i) = 0. (X . i) by RLVECT_1:15;
hence ||.((v2 - v0) . i).|| <= ||.((v1 - v0) . i).|| by A48; :: thesis:

end;

suppose i <> k1 ; :: thesis:

hence ||.((v2 - v0) . i).|| <= ||.((v1 - v0) . i).|| by A48, A49, LOPBAN10:16; :: thesis:

end;

hence (sqr (normsequence (X,w02))) . j <= (sqr (normsequence (X,w10))) . j by A46, A47, SQUARE_1:15; :: thesis:

end;

hence ||.(v2 - v0).|| <= ||.(v1 - v0).|| by A42, A43, A44, SQUARE_1:26, RVSUM_1:82; :: thesis:

end;

then A51: ||.(v2 - v0).|| <= 1 by A18, XXREAL_0:2;
A52: (len X) -' k = k1 by XREAL_0:def 2;
len (Cv0 | ((len X) -' k)) = k1 by A21, A36, A52, FINSEQ_1:59;
then A53: dom (Cv0 | ((len X) -' k)) = Seg k1 by FINSEQ_1:def 3;
len (Cv2 | ((len X) -' k)) = k1 by A36, A41, A52, FINSEQ_1:59;
then A54: dom (Cv2 | ((len X) -' k)) = Seg k1 by FINSEQ_1:def 3;
A55: (len X) -' (k + 1) = (len X) - (k + 1) by A18, XREAL_0:def 2, XREAL_1:48;
for j being Nat st j in dom (Cv0 | ((len X) -' k)) holds
(Cv0 | ((len X) -' k)) . j = (Cv2 | ((len X) -' k)) . j

proof

let j be Nat; :: thesis:
assume A56: j in dom (Cv0 | ((len X) -' k)) ; :: thesis:
then A57: (Cv0 | ((len X) -' k)) . j = Cv0 . j by FUNCT_1:47;
A59: ( 1 <= j & j <= k1 ) by A53, A56, FINSEQ_1:1;

per cases ;

suppose j = k1 ; :: thesis:

then Cv0 . j = Cv2 . j by LOPBAN10:15;
hence (Cv0 | ((len X) -' k)) . j = (Cv2 | ((len X) -' k)) . j by A53, A54, A56, A57, FUNCT_1:47; :: thesis:

end;

suppose A61: j <> k1 ; :: thesis:

then j < k1 by A59, XXREAL_0:1;
then j + 1 <= k1 by NAT_1:13;
then (j + 1) - 1 <= k1 - 1 by XREAL_1:13;
then A62: j in Seg ((len X) -' (k + 1)) by A55, A59;
j in dom X by A22, A56, RELAT_1:60, TARSKI:def 3;
then v2 . j = Cv1 . j by A61, LOPBAN10:16
.= (Cv0 | ((len X) -' (k + 1))) . j by A18, A62, FUNCT_1:49
.= v0 . j by A62, FUNCT_1:49 ;
hence (Cv0 | ((len X) -' k)) . j = (Cv2 | ((len X) -' k)) . j by A53, A54, A56, A57, FUNCT_1:47; :: thesis:

end;

then A63: Cv0 | ((len X) -' k) = Cv2 | ((len X) -' k) by A53, A54, FINSEQ_1:13;
consider F1 being FinSequence of REAL such that
A64: ( dom F1 = Seg k & ||.((f /. v2) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F1) & ( for n being Nat st n in Seg k holds
ex i being Element of dom X st
( i = ((len X) -' k) + n & F1 . n = ||.((v2 - v0) . i).|| ) ) ) by A17, A38, A51, A63;
||.(v1 - v2).|| <= ||.(v1 - v0).||

proof

A65: ||.(v1 - v2).|| = |.(normsequence (X,w12)).| by A3, PRVECT_2:def 12;
A66: ||.(v1 - v0).|| = |.(normsequence (X,w10)).| by A3, PRVECT_2:def 12;
A67: 0 <= Sum (sqr (normsequence (X,w12))) by RVSUM_1:86;
for j being Nat st j in Seg (len X) holds
(sqr (normsequence (X,w12))) . j <= (sqr (normsequence (X,w10))) . j

proof

let j be Nat; :: thesis:
assume A68: j in Seg (len X) ; :: thesis:
reconsider i = j as Element of dom X by A68, FINSEQ_1:def 3;
A69: (sqr (normsequence (X,w12))) . j = ((normsequence (X,w12)) . j) ^2 by VALUED_1:11
.= ||.((v1 - v2) . i).|| ^2 by PRVECT_2:def 11 ;
A70: (sqr (normsequence (X,w10))) . j = ((normsequence (X,w10)) . j) ^2 by VALUED_1:11
.= ||.((v1 - v0) . i).|| ^2 by PRVECT_2:def 11 ;
A71: (v1 - v2) . i = (v1 . i) - (v2 . i) by LOPBAN10:26;
||.((v1 - v2) . i).|| <= ||.((v1 - v0) . i).||

proof

per cases ;

suppose i = k1 ; :: thesis:

then v2 . i = v0 . i by LOPBAN10:15;
hence ||.((v1 - v2) . i).|| <= ||.((v1 - v0) . i).|| by A71, LOPBAN10:26; :: thesis:

end;

suppose i <> k1 ; :: thesis:

then v2 . i = v1 . i by LOPBAN10:16;
then (v1 . i) - (v2 . i) = 0. (X . i) by RLVECT_1:15;
hence ||.((v1 - v2) . i).|| <= ||.((v1 - v0) . i).|| by A71; :: thesis:

end;

hence (sqr (normsequence (X,w12))) . j <= (sqr (normsequence (X,w10))) . j by A69, A70, SQUARE_1:15; :: thesis:

end;

hence ||.(v1 - v2).|| <= ||.(v1 - v0).|| by A65, A66, A67, RVSUM_1:82, SQUARE_1:26; :: thesis:

end;

then A74: ||.(v1 - v2).|| <= 1 by A18, XXREAL_0:2;
for j being Element of dom X st k1 <> j holds
Cv1 . j = Cv2 . j by LOPBAN10:16;
then A75: ||.((f /. v1) - (f /. v2)).|| <= (((||.v2.|| + 1) |^ (len X)) * K) * ||.((v1 - v2) . k1).|| by A1, A2, A74, LM02;
v2 = v1 + (v2 - v1) by RLVECT_4:1;
then A76: ||.v2.|| <= ||.v1.|| + ||.(v2 - v1).|| by NORMSP_1:def 1;
||.(v2 - v1).|| <= 1 by A74, NORMSP_1:7;
then ||.v1.|| + ||.(v2 - v1).|| <= ||.v1.|| + 1 by XREAL_1:7;
then A77: ||.v2.|| <= ||.v1.|| + 1 by A76, XXREAL_0:2;
v1 = (v1 - v0) + v0 by RLVECT_4:1;
then ||.v1.|| <= ||.v0.|| + ||.(v1 - v0).|| by NORMSP_1:def 1;
then A78: ||.v1.|| <= ||.v0.|| + ||.(v0 - v1).|| by NORMSP_1:7;
||.(v0 - v1).|| <= 1 by A18, NORMSP_1:7;
then ||.v0.|| + ||.(v0 - v1).|| <= ||.v0.|| + 1 by XREAL_1:7;
then ||.v1.|| <= ||.v0.|| + 1 by A78, XXREAL_0:2;
then ||.v1.|| + 1 <= (||.v0.|| + 1) + 1 by XREAL_1:7;
then ||.v2.|| <= ||.v0.|| + 2 by A77, XXREAL_0:2;
then A79: ||.v2.|| + 1 <= (||.v0.|| + 2) + 1 by XREAL_1:7;
A80: (||.v2.|| + 1) |^ (len X) <= (||.v0.|| + 3) |^ (len X) by A79, PREPOWER:9;
A81: 0 < (||.v2.|| + 1) |^ (len X) by PREPOWER:6;
(v1 - v2) . k1 = (v1 . k1) - (v2 . k1) by LOPBAN10:26
.= (v1 . k1) - (v0 . k1) by LOPBAN10:15
.= (v1 - v0) . k1 by LOPBAN10:26 ;
then ((||.v2.|| + 1) |^ (len X)) * (K * ||.((v1 - v2) . k1).||) <= ((||.v0.|| + 3) |^ (len X)) * (K * ||.((v1 - v0) . k1).||) by A1, A80, A81, XREAL_1:66;
then A84: ||.((f /. v1) - (f /. v2)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * ||.((v1 - v0) . k1).|| by A75, XXREAL_0:2;
set F = <*||.((v1 - v0) . k1).||*> ^ F1;
rng (<*||.((v1 - v0) . k1).||*> ^ F1) c= REAL ;
then reconsider F = <*||.((v1 - v0) . k1).||*> ^ F1 as FinSequence of REAL by FINSEQ_1:def 4;
k is Element of NAT by ORDINAL1:def 12;
then A85: len F1 = k by A64, FINSEQ_1:def 3;
len F = (len F1) + (len <*||.((v1 - v0) . k1).||*>) by FINSEQ_1:22
.= k + 1 by A85, FINSEQ_1:40 ;
then A86: dom F = Seg (k + 1) by FINSEQ_1:def 3;
A87: for n being Nat st n in Seg (k + 1) holds
ex i being Element of dom X st
( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

proof

let n be Nat; :: thesis:
assume n in Seg (k + 1) ; :: thesis:
then A88: ( 1 <= n & n <= k + 1 ) by FINSEQ_1:1;

per cases ;

suppose A89: n = 1 ; :: thesis:

then A90: ((len X) -' (k + 1)) + n = ((len X) - (k + 1)) + 1 by A18, XREAL_0:def 2, XREAL_1:48
.= k1 ;
take k1 ; :: thesis:
thus ( k1 = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . k1).|| ) by A89, A90, FINSEQ_1:41; :: thesis:

end;

suppose n <> 1 ; :: thesis:

then 1 < n by A88, XXREAL_0:1;
then A91: 1 + 1 <= n by NAT_1:13;
A93: ((len X) - (k + 1)) + n <= ((len X) - (k + 1)) + (k + 1) by A88, XREAL_1:7;
A94: ((len X) - (k + 1)) + 2 <= ((len X) - (k + 1)) + n by A91, XREAL_1:7;
1 + 0 <= 1 + ((len X) - k) by A35, XREAL_1:7;
then 1 <= ((len X) -' (k + 1)) + n by A55, A94, XXREAL_0:2;
then ((len X) -' (k + 1)) + n in Seg (len X) by A55, A93;
then reconsider i = ((len X) -' (k + 1)) + n as Element of dom X by FINSEQ_1:def 3;
take i ; :: thesis:
thus i = ((len X) -' (k + 1)) + n ; :: thesis:
A95: 2 - 1 <= n - 1 by A91, XREAL_1:9;
A96: n - 1 <= (k + 1) - 1 by A88, XREAL_1:9;
reconsider n1 = n - 1 as Element of NAT by A88, INT_1:3;
A97: n1 in Seg k by A95, A96;
A98: len <*||.((v1 - v0) . k1).||*> = 1 by FINSEQ_1:40;
A100: F . n = F . (1 + n1)
.= F1 . n1 by A85, A95, A96, A98, FINSEQ_1:65 ;
consider i1 being Element of dom X such that
A101: ( i1 = ((len X) -' k) + n1 & F1 . n1 = ||.((v2 - v0) . i1).|| ) by A64, A97;
A102: i1 = ((len X) - (k + 1)) + n by A52, A101
.= i by A18, XREAL_0:def 2, XREAL_1:48 ;
A105: k1 + 0 < k1 + 1 by XREAL_1:8;
A106: k1 + 1 <= k1 + n1 by A95, XREAL_1:7;
(v2 - v0) . i = (v2 . i) - (v0 . i) by LOPBAN10:26
.= (v1 . i) - (v0 . i) by A52, A101, A102, A105, A106, LOPBAN10:16
.= (v1 - v0) . i by LOPBAN10:26 ;
hence F . n = ||.((v1 - v0) . i).|| by A100, A101, A102; :: thesis:

end;

(f /. v1) - (f /. v0) = (((f /. v1) - (f /. v2)) + (f /. v2)) - (f /. v0) by RLVECT_4:1
.= ((f /. v1) - (f /. v2)) + ((f /. v2) - (f /. v0)) by RLVECT_1:28 ;
then A107: ||.((f /. v1) - (f /. v0)).|| <= ||.((f /. v1) - (f /. v2)).|| + ||.((f /. v2) - (f /. v0)).|| by NORMSP_1:def 1;
A108: ||.((f /. v1) - (f /. v2)).|| + ||.((f /. v2) - (f /. v0)).|| <= ((((||.v0.|| + 3) |^ (len X)) * K) * ||.((v1 - v0) . k1).||) + ((((||.v0.|| + 3) |^ (len X)) * K) * (Sum F1)) by A64, A84, XREAL_1:7;
((((||.v0.|| + 3) |^ (len X)) * K) * ||.((v1 - v0) . k1).||) + ((((||.v0.|| + 3) |^ (len X)) * K) * (Sum F1)) = (((||.v0.|| + 3) |^ (len X)) * K) * (||.((v1 - v0) . k1).|| + (Sum F1))
.= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) by RVSUM_1:76 ;
hence ex F being FinSequence of REAL st
( dom F = Seg (k + 1) & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( for n being Nat st n in Seg (k + 1) holds
ex i being Element of dom X st
( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| ) ) ) by A86, A87, A107, A108, XXREAL_0:2; :: thesis:

end;

A109: for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A16);
let v1 be Point of (product X); :: thesis:
assume A110: ||.(v1 - v0).|| <= 1 ; :: thesis:
consider g being Function such that
A111: ( v1 = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds
g . i in (carr X) . i ) ) by A3, CARD_3:def 5;
dom g = Seg (len (carr X)) by A111, FINSEQ_1:def 3;
then reconsider Cv1 = v1 as FinSequence by A111, FINSEQ_1:def 2;
A112: (len X) -' (len X) = (0 + (len X)) -' (len X)
.= 0 by NAT_D:34 ;
Cv1 | ((len X) -' (len X)) = {} by A112
.= Cv0 | ((len X) -' (len X)) by A112 ;
then consider F being FinSequence of REAL such that
A113: ( dom F = Seg (len X) & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( for n being Nat st n in Seg (len X) holds
ex i being Element of dom X st
( i = ((len X) -' (len X)) + n & F . n = ||.((v1 - v0) . i).|| ) ) ) by A109, A110;
for i being Element of dom X holds F . i = ||.((v1 - v0) . i).||

proof

let i be Element of dom X; :: thesis:
i in dom X ;
then A116: i in Seg (len X) by FINSEQ_1:def 3;
reconsider n = i as Nat ;
consider j being Element of dom X such that
A117: ( j = ((len X) -' (len X)) + n & F . n = ||.((v1 - v0) . j).|| ) by A113, A116;
thus F . i = ||.((v1 - v0) . i).|| by A112, A117; :: thesis:

end;

hence ex F being FinSequence of REAL st
( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) by A113, FINSEQ_1:def 3; :: thesis: