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, v1 being Point of ()
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) holds
||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((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, v1 being Point of ()
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) holds
||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((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, v1 being Point of ()
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) holds
||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let K be Real; :: thesis: ( 0 <= K & ( for x being Point of () holds ||.(f . x).|| <= K * () ) implies for v0, v1 being Point of ()
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) holds
||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| )

assume A1: ( 0 <= K & ( for x being Point of () holds ||.(f . x).|| <= K * () ) ) ; :: thesis: for v0, v1 being Point of ()
for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) holds
||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let v0, v1 be Point of (); :: thesis: for Cv0, Cv1 being FinSequence
for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) holds
||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let Cv0, Cv1 be FinSequence; :: thesis: for i being Element of dom X st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) holds
||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||

let i be Element of dom X; :: thesis: ( Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) implies ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| )

assume A2: ( Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & ( for j being Element of dom X st i <> j holds
Cv1 . j = Cv0 . j ) ) ; :: thesis: ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).||
( f is Function of (),Y & f is Multilinear ) ;
then A3: f * (reproj (i,v0)) is LinearOperator of (X . i),Y ;
A4: product X = NORMSTR(# (product (carr X)),(),[:():],[:():],() #) by PRVECT_2:6;
then A5: ex g being Function st
( Cv1 = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds
g . i in (carr X) . i ) ) by ;
A6: ex g being Function st
( (reproj (i,v0)) . (v1 . i) = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds
g . i in (carr X) . i ) ) by ;
for x being object st x in dom v1 holds
v1 . x = ((reproj (i,v0)) . (v1 . i)) . x
proof
let x be object ; :: thesis: ( x in dom v1 implies v1 . x = ((reproj (i,v0)) . (v1 . i)) . x )
assume x in dom v1 ; :: thesis: v1 . x = ((reproj (i,v0)) . (v1 . i)) . x
then reconsider j = x as Element of dom X by ;
per cases ( j = i or j <> i ) ;
suppose j = i ; :: thesis: v1 . x = ((reproj (i,v0)) . (v1 . i)) . x
hence v1 . x = ((reproj (i,v0)) . (v1 . i)) . x by LOPBAN10:15; :: thesis: verum
end;
suppose A8: j <> i ; :: thesis: v1 . x = ((reproj (i,v0)) . (v1 . i)) . x
then ((reproj (i,v0)) . (v1 . i)) . j = v0 . j by LOPBAN10:16
.= v1 . j by A2, A8 ;
hence v1 . x = ((reproj (i,v0)) . (v1 . i)) . x ; :: thesis: verum
end;
end;
end;
then A10: v1 = (reproj (i,v0)) . (v1 . i) by ;
reconsider v3 = (reproj (i,v0)) . ((v1 . i) - (v0 . i)) as Point of () ;
(f /. v1) - (f /. v0) = (f . ((reproj (i,v0)) . (v1 . i))) - (f . ((reproj (i,v0)) . (v0 . i))) by
.= ((f * (reproj (i,v0))) . (v1 . i)) - (f . ((reproj (i,v0)) . (v0 . i))) by FUNCT_2:15
.= ((f * (reproj (i,v0))) . (v1 . i)) - ((f * (reproj (i,v0))) . (v0 . i)) by FUNCT_2:15
.= ((f * (reproj (i,v0))) . (v1 . i)) + ((- 1) * ((f * (reproj (i,v0))) . (v0 . i))) by RLVECT_1:16
.= ((f * (reproj (i,v0))) . (v1 . i)) + ((f * (reproj (i,v0))) . ((- 1) * (v0 . i))) by
.= (f * (reproj (i,v0))) . ((v1 . i) + ((- 1) * (v0 . i))) by
.= (f * (reproj (i,v0))) . ((v1 . i) - (v0 . i)) by RLVECT_1:16
.= f . v3 by FUNCT_2:15 ;
then A12: ||.((f /. v1) - (f /. v0)).|| <= K * () by A1;
1 is Element of REAL by XREAL_0:def 1;
then reconsider R1 = (len X) |-> 1 as FinSequence of REAL by FINSEQ_2:63;
A13: dom R1 = Seg (len X) by FUNCT_2:def 1;
i in dom X ;
then A14: i in dom R1 by ;
reconsider Nv1v0 = ||.((v1 - v0) . i).|| as Element of REAL ;
reconsider R2 = R1 +* (i,Nv1v0) as FinSequence of REAL ;
||.v0.|| + 1 is Element of REAL by XREAL_0:def 1;
then reconsider R3 = (len X) |-> (||.v0.|| + 1) as FinSequence of REAL by FINSEQ_2:63;
set R4 = mlt (R2,R3);
dom R2 = dom R1 by FUNCT_7:30;
then ( dom R2 = Seg (len X) & dom R3 = Seg (len X) ) by FUNCT_2:def 1;
then A15: ( len R2 = len X & len R3 = len X ) by FINSEQ_1:def 3;
then ( R2 is Element of (len X) -tuples_on REAL & R3 is Element of (len X) -tuples_on REAL ) by FINSEQ_2:92;
then A16: Product (mlt (R2,R3)) = (Product R2) * (Product R3) by RVSUM_1:107;
A17: Product R2 = ||.((v1 - v0) . i).|| by ;
A18: Product R3 = (||.v0.|| + 1) to_power (len X) by NAT_4:55
.= (||.v0.|| + 1) |^ (len X) ;
consider Nx being FinSequence of REAL such that
A19: ( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(v3 . i).|| ) & NrProduct v3 = Product Nx ) by LOPBAN10:def 9;
dom Nx = Seg (len X) by ;
then A20: len Nx = len X by FINSEQ_1:def 3;
dom (mlt (R2,R3)) = (dom R2) /\ (dom R3) by VALUED_1:def 4
.= (Seg (len R2)) /\ (dom R3) by FINSEQ_1:def 3
.= (Seg (len R2)) /\ (Seg (len R3)) by FINSEQ_1:def 3
.= Seg (len X) by A15 ;
then A21: len (mlt (R2,R3)) = len X by FINSEQ_1:def 3;
for k being Element of NAT st k in dom Nx holds
( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k )
proof
let k be Element of NAT ; :: thesis: ( k in dom Nx implies ( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k ) )
assume k in dom Nx ; :: thesis: ( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k )
then A22: k in Seg (len Nx) by FINSEQ_1:def 3;
then reconsider j = k as Element of dom X by ;
A24: Nx . k = ||.(v3 . j).|| by A19;
A26: (mlt (R2,R3)) . k = (R2 . k) * (R3 . j) by RVSUM_1:60
.= (R2 . k) * (||.v0.|| + 1) by ;
now :: thesis: Nx . k <= (mlt (R2,R3)) . k
per cases ( j = i or j <> i ) ;
suppose A27: j = i ; :: thesis: Nx . k <= (mlt (R2,R3)) . k
v3 . j = (v1 . i) - (v0 . i) by
.= (v1 - v0) . i by LOPBAN10:26 ;
then A29: Nx . k = ||.((v1 - v0) . i).|| by ;
1 + 0 <= ||.v0.|| + 1 by XREAL_1:7;
then ||.((v1 - v0) . i).|| * 1 <= ||.((v1 - v0) . i).|| * (||.v0.|| + 1) by XREAL_1:66;
hence Nx . k <= (mlt (R2,R3)) . k by ; :: thesis: verum
end;
suppose A30: j <> i ; :: thesis: Nx . k <= (mlt (R2,R3)) . k
then A31: R2 . k = R1 . j by FUNCT_7:32
.= 1 by ;
||.(v0 . j).|| <= ||.v0.|| by ;
then ||.(v0 . j).|| + 0 <= ||.v0.|| + 1 by XREAL_1:7;
hence Nx . k <= (mlt (R2,R3)) . k by ; :: thesis: verum
end;
end;
end;
hence ( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k ) by A24; :: thesis: verum
end;
then NrProduct v3 <= ||.((v1 - v0) . i).|| * ((||.v0.|| + 1) |^ (len X)) by ;
then K * () <= K * (((||.v0.|| + 1) |^ (len X)) * ||.((v1 - v0) . i).||) by ;
hence ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| by ; :: thesis: verum