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 () holds ||.(f . x).|| <= K * () ) holds
for v0 being Point of () ex M being Real st
( 0 <= M & ( for v1 being Point of () 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 () holds ||.(f . x).|| <= K * () ) holds
for v0 being Point of () ex M being Real st
( 0 <= M & ( for v1 being Point of () 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 () holds ||.(f . x).|| <= K * () ) holds
for v0 being Point of () ex M being Real st
( 0 <= M & ( for v1 being Point of () 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 () holds ||.(f . x).|| <= K * () ) implies for v0 being Point of () ex M being Real st
( 0 <= M & ( for v1 being Point of () 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 () holds ||.(f . x).|| <= K * () ; :: thesis: for v0 being Point of () ex M being Real st
( 0 <= M & ( for v1 being Point of () 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)),(),[:():],[:():],() #) by PRVECT_2:6;
let v0 be Point of (); :: thesis: ex M being Real st
( 0 <= M & ( for v1 being Point of () 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 ;
dom g = Seg (len (carr X)) by ;
then reconsider Cv0 = v0 as FinSequence by ;
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 () 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 () 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 S1[ Nat] means for v0, v1 being Point of ()
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: S1[ 0 ]
proof
let v0, v1 be Point of (); :: 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 ;
A10: dom g = Seg (len (carr X)) by ;
then reconsider Cv0 = v0 as FinSequence by ;
A11: len Cv0 = len (carr X) by
.= 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 ;
dom Cv1 = Seg (len (carr X)) by ;
then A14: len Cv1 = len (carr X) by FINSEQ_1:def 3
.= len X by PRVECT_2:def 4 ;
Cv1 = Cv0 | (len X) by
.= Cv0 by ;
then (f /. v1) - (f /. v0) = 0. Y by ;
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;
A16: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A17: S1[k] ; :: thesis: S1[k + 1]
let v0, v1 be Point of (); :: 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 ;
dom g = Seg (len (carr X)) by ;
then reconsider Cv0 = v0 as FinSequence by ;
dom Cv0 = Seg (len (carr X)) by ;
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 ;
dom g1 = Seg (len (carr X)) by ;
then reconsider Cv1 = v1 as FinSequence by ;
1 <= 1 + k by NAT_1:11;
then 1 <= len X by ;
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 ) ;
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).|| ) ) )

then A26: (len X) -' (k + 1) = (len X) - 1 by ;
for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j
proof
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 ;
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 ;
thus Cv1 . j = (Cv0 | ((len X) -' (k + 1))) . j by
.= Cv0 . j by ; :: thesis: verum
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: ( 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 ; :: 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 ;
(||.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 ;
hence ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * (Sum F) by ; :: 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
.= i ;
take i ; :: thesis: ( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )
n = 1 by ;
hence ( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| ) by ; :: thesis: verum
end;
end;
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).|| ) ) )

A35: (k + 1) - k <= (len X) - k by ;
A36: (len X) - k <= (len X) - 0 by XREAL_1:13;
(len X) - k in NAT by ;
then (len X) - k in Seg (len X) by ;
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 ;
reconsider v2 = (reproj (k1,v1)) . Cv0k1 as Point of () ;
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 ;
A40: dom g = Seg (len (carr X)) by ;
then reconsider Cv2 = v2 as FinSequence by ;
A41: len Cv2 = len (carr X) by
.= 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
A42: ||.(v2 - v0).|| = |.(normsequence (X,w02)).| by ;
A43: ||.(v1 - v0).|| = |.(normsequence (X,w10)).| by ;
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: ( 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 ;
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 ( i = k1 or i <> k1 ) ;
suppose A50: i = k1 ; :: thesis: ||.((v2 - v0) . i).|| <= ||.((v1 - v0) . i).||
v2 . i = v0 . i by ;
then (v2 . i) - (v0 . i) = 0. (X . i) by RLVECT_1:15;
hence ||.((v2 - v0) . i).|| <= ||.((v1 - v0) . i).|| by A48; :: thesis: verum
end;
suppose i <> k1 ; :: thesis: ||.((v2 - v0) . i).|| <= ||.((v1 - v0) . i).||
hence ||.((v2 - v0) . i).|| <= ||.((v1 - v0) . i).|| by ; :: thesis: verum
end;
end;
end;
hence (sqr (normsequence (X,w02))) . j <= (sqr (normsequence (X,w10))) . j by ; :: thesis: verum
end;
hence ||.(v2 - v0).|| <= ||.(v1 - v0).|| by ; :: thesis: verum
end;
then A51: ||.(v2 - v0).|| <= 1 by ;
A52: (len X) -' k = k1 by XREAL_0:def 2;
len (Cv0 | ((len X) -' k)) = k1 by ;
then A53: dom (Cv0 | ((len X) -' k)) = Seg k1 by FINSEQ_1:def 3;
len (Cv2 | ((len X) -' k)) = k1 by ;
then A54: dom (Cv2 | ((len X) -' k)) = Seg k1 by FINSEQ_1:def 3;
A55: (len X) -' (k + 1) = (len X) - (k + 1) by ;
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: ( 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 ;
per cases ( j = k1 or j <> k1 ) ;
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 ; :: thesis: verum
end;
suppose A61: j <> k1 ; :: thesis: (Cv0 | ((len X) -' k)) . j = (Cv2 | ((len X) -' k)) . j
then j < k1 by ;
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 ;
j in dom X by ;
then v2 . j = Cv1 . j by
.= (Cv0 | ((len X) -' (k + 1))) . j by
.= v0 . j by ;
hence (Cv0 | ((len X) -' k)) . j = (Cv2 | ((len X) -' k)) . j by ; :: thesis: verum
end;
end;
end;
then A63: Cv0 | ((len X) -' k) = Cv2 | ((len X) -' k) by ;
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 ;
A66: ||.(v1 - v0).|| = |.(normsequence (X,w10)).| by ;
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: ( 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 ;
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 ( i = k1 or i <> k1 ) ;
suppose i = k1 ; :: thesis: ||.((v1 - v2) . i).|| <= ||.((v1 - v0) . i).||
then v2 . i = v0 . i by LOPBAN10:15;
hence ||.((v1 - v2) . i).|| <= ||.((v1 - v0) . i).|| by ; :: thesis: verum
end;
suppose i <> k1 ; :: thesis: ||.((v1 - v2) . i).|| <= ||.((v1 - v0) . i).||
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: verum
end;
end;
end;
hence (sqr (normsequence (X,w12))) . j <= (sqr (normsequence (X,w10))) . j by ; :: thesis: verum
end;
hence ||.(v1 - v2).|| <= ||.(v1 - v0).|| by ; :: thesis: verum
end;
then A74: ||.(v1 - v2).|| <= 1 by ;
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 ;
then ||.v1.|| + ||.(v2 - v1).|| <= ||.v1.|| + 1 by XREAL_1:7;
then A77: ||.v2.|| <= ||.v1.|| + 1 by ;
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 ;
then ||.v0.|| + ||.(v0 - v1).|| <= ||.v0.|| + 1 by XREAL_1:7;
then ||.v1.|| <= ||.v0.|| + 1 by ;
then ||.v1.|| + 1 <= (||.v0.|| + 1) + 1 by XREAL_1:7;
then ||.v2.|| <= ||.v0.|| + 2 by ;
then A79: ||.v2.|| + 1 <= (||.v0.|| + 2) + 1 by XREAL_1:7;
A80: (||.v2.|| + 1) |^ (len X) <= (||.v0.|| + 3) |^ (len X) by ;
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 ;
then A84: ||.((f /. v1) - (f /. v2)).|| <= (((||.v0.|| + 3) |^ (len X)) * K) * ||.((v1 - v0) . k1).|| by ;
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 ;
len F = (len F1) + (len <*||.((v1 - v0) . k1).||*>) by FINSEQ_1:22
.= k + 1 by ;
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: ( 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;
per cases ( n = 1 or n <> 1 ) ;
suppose A89: n = 1 ; :: thesis: ex i being Element of dom X st
( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

then A90: ((len X) -' (k + 1)) + n = ((len X) - (k + 1)) + 1 by
.= 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 ; :: thesis: verum
end;
suppose n <> 1 ; :: thesis: ex i being Element of dom X st
( i = ((len X) -' (k + 1)) + n & F . n = ||.((v1 - v0) . i).|| )

then 1 < n by ;
then A91: 1 + 1 <= n by NAT_1:13;
A93: ((len X) - (k + 1)) + n <= ((len X) - (k + 1)) + (k + 1) by ;
A94: ((len X) - (k + 1)) + 2 <= ((len X) - (k + 1)) + n by ;
1 + 0 <= 1 + ((len X) - k) by ;
then 1 <= ((len X) -' (k + 1)) + n by ;
then ((len X) -' (k + 1)) + n in Seg (len X) by ;
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 ;
A96: n - 1 <= (k + 1) - 1 by ;
reconsider n1 = n - 1 as Element of NAT by ;
A97: n1 in Seg k by ;
A98: len <*||.((v1 - v0) . k1).||*> = 1 by FINSEQ_1:40;
A100: F . n = F . (1 + n1)
.= F1 . n1 by ;
consider i1 being Element of dom X such that
A101: ( i1 = ((len X) -' k) + n1 & F1 . n1 = ||.((v2 - v0) . i1).|| ) by ;
A102: i1 = ((len X) - (k + 1)) + n by
.= i by ;
A105: k1 + 0 < k1 + 1 by XREAL_1:8;
A106: k1 + 1 <= k1 + n1 by ;
(v2 - v0) . i = (v2 . i) - (v0 . i) by LOPBAN10:26
.= (v1 . i) - (v0 . i) by
.= (v1 - v0) . i by LOPBAN10:26 ;
hence F . n = ||.((v1 - v0) . i).|| by ; :: thesis: verum
end;
end;
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 ;
((((||.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 ; :: thesis: verum
end;
end;
end;
A109: for n being Nat holds S1[n] from NAT_1:sch 2(A6, A16);
let v1 be Point of (); :: 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 ;
dom g = Seg (len (carr X)) by ;
then reconsider Cv1 = v1 as FinSequence by ;
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 ;
for i being Element of dom X holds F . i = ||.((v1 - v0) . i).||
proof
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 ;
thus F . i = ||.((v1 - v0) . i).|| by ; :: thesis: verum
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 ; :: thesis: verum