let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace

for f being MultilinearOperator of X,Y

for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0 being Point of (product X) ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )

let Y be RealNormSpace; :: thesis: for f being MultilinearOperator of X,Y

for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0 being Point of (product X) ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )

let f be MultilinearOperator of X,Y; :: thesis: for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0 being Point of (product X) ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )

let K be Real; :: thesis: ( 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) implies for v0 being Point of (product X) ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) ) )

assume that

A1: 0 <= K and

A2: for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ; :: thesis: for v0 being Point of (product X) ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )

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: ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )

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: ( 0 <= (||.v0.|| + 3) |^ (len X) & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

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).|| ) ) ) )

thus 0 <= (||.v0.|| + 3) |^ (len X) by POWER:3; :: thesis: for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

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).|| ) )

defpred S_{1}[ 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_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[n]
from NAT_1:sch 2(A6, A16);

let v1 be Point of (product X); :: thesis: ( ||.(v1 - v0).|| <= 1 implies 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).|| ) ) )

assume A110: ||.(v1 - v0).|| <= 1 ; :: thesis: 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).|| ) )

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).||

( 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: verum

for f being MultilinearOperator of X,Y

for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0 being Point of (product X) ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )

let Y be RealNormSpace; :: thesis: for f being MultilinearOperator of X,Y

for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0 being Point of (product X) ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )

let f be MultilinearOperator of X,Y; :: thesis: for K being Real st 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) holds

for v0 being Point of (product X) ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )

let K be Real; :: thesis: ( 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) implies for v0 being Point of (product X) ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) ) )

assume that

A1: 0 <= K and

A2: for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ; :: thesis: for v0 being Point of (product X) ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )

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: ex M being Real st

( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) )

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: ( 0 <= (||.v0.|| + 3) |^ (len X) & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

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).|| ) ) ) )

thus 0 <= (||.v0.|| + 3) |^ (len X) by POWER:3; :: thesis: for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

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).|| ) )

defpred S

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

proof

A16:
for k being Nat st S
let v0, v1 be Point of (product X); :: thesis: for Cv0, Cv1 being FinSequence st ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & 0 <= len X & Cv1 | ((len X) -' 0) = Cv0 | ((len X) -' 0) holds

ex F being FinSequence of REAL st

( dom F = Seg 0 & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( 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).|| ) ) )

let Cv0, Cv1 be FinSequence; :: thesis: ( ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & 0 <= len X & Cv1 | ((len X) -' 0) = Cv0 | ((len X) -' 0) implies ex F being FinSequence of REAL st

( dom F = Seg 0 & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( 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).|| ) ) ) )

assume A7: ( ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & 0 <= len X & Cv1 | ((len X) -' 0) = Cv0 | ((len X) -' 0) ) ; :: thesis: ex F being FinSequence of REAL st

( dom F = Seg 0 & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( 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).|| ) ) )

A8: (len X) -' 0 = ((len X) + 0) -' 0

.= len X by NAT_D:34 ;

reconsider F = <*> REAL as FinSequence of REAL ;

take F ; :: thesis: ( dom F = Seg 0 & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( 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).|| ) ) )

thus dom F = Seg 0 ; :: thesis: ( ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( 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).|| ) ) )

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_2:def 4 ;

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_2:def 4 ;

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: 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).|| )

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: verum

end;ex F being FinSequence of REAL st

( dom F = Seg 0 & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( 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).|| ) ) )

let Cv0, Cv1 be FinSequence; :: thesis: ( ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & 0 <= len X & Cv1 | ((len X) -' 0) = Cv0 | ((len X) -' 0) implies ex F being FinSequence of REAL st

( dom F = Seg 0 & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( 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).|| ) ) ) )

assume A7: ( ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & 0 <= len X & Cv1 | ((len X) -' 0) = Cv0 | ((len X) -' 0) ) ; :: thesis: ex F being FinSequence of REAL st

( dom F = Seg 0 & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( 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).|| ) ) )

A8: (len X) -' 0 = ((len X) + 0) -' 0

.= len X by NAT_D:34 ;

reconsider F = <*> REAL as FinSequence of REAL ;

take F ; :: thesis: ( dom F = Seg 0 & ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( 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).|| ) ) )

thus dom F = Seg 0 ; :: thesis: ( ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) & ( 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).|| ) ) )

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_2:def 4 ;

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_2:def 4 ;

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: 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).|| )

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: verum

S

proof

A109:
for n being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A17: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let v0, v1 be Point of (product X); :: thesis: for Cv0, Cv1 being FinSequence st ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & k + 1 <= len X & Cv1 | ((len X) -' (k + 1)) = Cv0 | ((len X) -' (k + 1)) holds

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).|| ) ) )

let Cv0, Cv1 be FinSequence; :: thesis: ( ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & k + 1 <= len X & Cv1 | ((len X) -' (k + 1)) = Cv0 | ((len X) -' (k + 1)) implies 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).|| ) ) ) )

assume A18: ( ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & k + 1 <= len X & Cv1 | ((len X) -' (k + 1)) = Cv0 | ((len X) -' (k + 1)) ) ; :: thesis: 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).|| ) ) )

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_2:def 4 ;

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;

end;assume A17: S

let v0, v1 be Point of (product X); :: thesis: for Cv0, Cv1 being FinSequence st ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & k + 1 <= len X & Cv1 | ((len X) -' (k + 1)) = Cv0 | ((len X) -' (k + 1)) holds

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).|| ) ) )

let Cv0, Cv1 be FinSequence; :: thesis: ( ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & k + 1 <= len X & Cv1 | ((len X) -' (k + 1)) = Cv0 | ((len X) -' (k + 1)) implies 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).|| ) ) ) )

assume A18: ( ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & k + 1 <= len X & Cv1 | ((len X) -' (k + 1)) = Cv0 | ((len X) -' (k + 1)) ) ; :: thesis: 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).|| ) ) )

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_2:def 4 ;

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
( k = 0 or k <> 0 )
;

end;

suppose A25:
k = 0
; :: thesis: 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).|| ) ) )

( 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).|| ) ) )

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

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: ( 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).|| ) ) )

thus dom F = Seg (len F) by FINSEQ_1:def 3

.= Seg (k + 1) by A25, FINSEQ_1:40 ; :: thesis: ( ||.((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).|| ) ) )

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: 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).|| )

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: verum

end;for j being Element of dom X st i <> j holds

Cv1 . j = Cv0 . j

proof

then A29:
||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||
by A1, A2, A18, LM02;
let j be Element of dom X; :: thesis: ( i <> j implies Cv1 . j = Cv0 . j )

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: Cv1 . j = Cv0 . j

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: verum

end;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: Cv1 . j = Cv0 . j

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: verum

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: ( 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).|| ) ) )

thus dom F = Seg (len F) by FINSEQ_1:def 3

.= Seg (k + 1) by A25, FINSEQ_1:40 ; :: thesis: ( ||.((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).|| ) ) )

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: 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).|| )

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: verum

proof

let n be Nat; :: thesis: ( n in Seg (k + 1) implies ex j being Element of dom X st

( j = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . j).|| ) )

assume A33: n in Seg (k + 1) ; :: thesis: ex j being Element of dom X st

( j = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . j).|| )

then A34: ((len X) -' (k + 1)) + n = ((len X) - 1) + 1 by A25, A26, FINSEQ_1:2, TARSKI:def 1

.= i ;

take i ; :: thesis: ( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

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: verum

end;( j = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . j).|| ) )

assume A33: n in Seg (k + 1) ; :: thesis: ex j being Element of dom X st

( j = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . j).|| )

then A34: ((len X) -' (k + 1)) + n = ((len X) - 1) + 1 by A25, A26, FINSEQ_1:2, TARSKI:def 1

.= i ;

take i ; :: thesis: ( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

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: verum

suppose
k <> 0
; :: thesis: 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).|| ) ) )

( 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).|| ) ) )

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_2:def 4 ;

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).||

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

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).||

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).|| )

.= ((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: verum

end;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_2:def 4 ;

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

then A51:
||.(v2 - v0).|| <= 1
by A18, XXREAL_0:2;
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

end;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

hence
||.(v2 - v0).|| <= ||.(v1 - v0).||
by A42, A43, A44, SQUARE_1:26, RVSUM_1:82; :: thesis: verum
let j be Nat; :: thesis: ( j in Seg (len X) implies (sqr (normsequence (X,w02))) . j <= (sqr (normsequence (X,w10))) . j )

assume A45: j in Seg (len X) ; :: thesis: (sqr (normsequence (X,w02))) . j <= (sqr (normsequence (X,w10))) . j

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).||

end;assume A45: j in Seg (len X) ; :: thesis: (sqr (normsequence (X,w02))) . j <= (sqr (normsequence (X,w10))) . j

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
end;

hence
(sqr (normsequence (X,w02))) . j <= (sqr (normsequence (X,w10))) . j
by A46, A47, SQUARE_1:15; :: thesis: verumA52: (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

then A63:
Cv0 | ((len X) -' k) = Cv2 | ((len X) -' k)
by A53, A54, FINSEQ_1:13;
let j be Nat; :: thesis: ( j in dom (Cv0 | ((len X) -' k)) implies (Cv0 | ((len X) -' k)) . j = (Cv2 | ((len X) -' k)) . j )

assume A56: j in dom (Cv0 | ((len X) -' k)) ; :: thesis: (Cv0 | ((len X) -' k)) . j = (Cv2 | ((len X) -' k)) . j

then A57: (Cv0 | ((len X) -' k)) . j = Cv0 . j by FUNCT_1:47;

A59: ( 1 <= j & j <= k1 ) by A53, A56, FINSEQ_1:1;

end;assume A56: j in dom (Cv0 | ((len X) -' k)) ; :: thesis: (Cv0 | ((len X) -' k)) . j = (Cv2 | ((len X) -' k)) . j

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
( j = k1 or j <> k1 )
;

end;

suppose
j = k1
; :: thesis: (Cv0 | ((len X) -' k)) . j = (Cv2 | ((len X) -' k)) . j

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: verum

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

suppose A61:
j <> k1
; :: thesis: (Cv0 | ((len X) -' k)) . j = (Cv2 | ((len X) -' k)) . j

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: verum

end;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: verum

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

then A74:
||.(v1 - v2).|| <= 1
by A18, XXREAL_0:2;
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

end;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

hence
||.(v1 - v2).|| <= ||.(v1 - v0).||
by A65, A66, A67, RVSUM_1:82, SQUARE_1:26; :: thesis: verum
let j be Nat; :: thesis: ( j in Seg (len X) implies (sqr (normsequence (X,w12))) . j <= (sqr (normsequence (X,w10))) . j )

assume A68: j in Seg (len X) ; :: thesis: (sqr (normsequence (X,w12))) . j <= (sqr (normsequence (X,w10))) . j

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).||

end;assume A68: j in Seg (len X) ; :: thesis: (sqr (normsequence (X,w12))) . j <= (sqr (normsequence (X,w10))) . j

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
end;

hence
(sqr (normsequence (X,w12))) . j <= (sqr (normsequence (X,w10))) . j
by A69, A70, SQUARE_1:15; :: thesis: verumfor 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

(f /. v1) - (f /. v0) =
(((f /. v1) - (f /. v2)) + (f /. v2)) - (f /. v0)
by RLVECT_4:1
let n be Nat; :: thesis: ( n in Seg (k + 1) implies ex i being Element of dom X st

( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| ) )

assume n in Seg (k + 1) ; :: thesis: ex i being Element of dom X st

( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

then A88: ( 1 <= n & n <= k + 1 ) by FINSEQ_1:1;

end;( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| ) )

assume n in Seg (k + 1) ; :: thesis: ex i being Element of dom X st

( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

then A88: ( 1 <= n & n <= k + 1 ) by FINSEQ_1:1;

per cases
( n = 1 or n <> 1 )
;

end;

suppose A89:
n = 1
; :: thesis: ex i being Element of dom X st

( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

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: ( k1 = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . k1).|| )

thus ( k1 = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . k1).|| ) by A89, A90, FINSEQ_1:41; :: thesis: verum

end;.= k1 ;

take k1 ; :: thesis: ( k1 = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . k1).|| )

thus ( k1 = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . k1).|| ) by A89, A90, FINSEQ_1:41; :: thesis: verum

suppose
n <> 1
; :: thesis: ex i being Element of dom X st

( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

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: ( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

thus i = ((len X) -' (k + 1)) + n ; :: thesis: F . n = ||.((v1 - v0) . i).||

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: verum

end;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: ( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

thus i = ((len X) -' (k + 1)) + n ; :: thesis: F . n = ||.((v1 - v0) . i).||

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: verum

.= ((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: verum

let v1 be Point of (product X); :: thesis: ( ||.(v1 - v0).|| <= 1 implies 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).|| ) ) )

assume A110: ||.(v1 - v0).|| <= 1 ; :: thesis: 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).|| ) )

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

hence
ex F being FinSequence of REAL st
let i be Element of dom X; :: thesis: F . i = ||.((v1 - v0) . i).||

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: verum

end;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: verum

( 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: verum