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 A1: ( 0 <= K & ( for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ) ) ; :: thesis:
let v0, v1 be Point of (product X); :: thesis:
let Cv0, Cv1 be FinSequence; :: thesis:
let i be Element of dom X; :: thesis:
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 is Function of (product X),Y & f is Multilinear ) ;
then A3: f * (reproj (i,v0)) is LinearOperator of (X . i),Y ;
A4: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm 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 A2, CARD_3:def 5;
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 A4, CARD_3:def 5;
for x being object st x in dom v1 holds
v1 . x = ((reproj (i,v0)) . (v1 . i)) . x

proof

let x be object ; :: thesis:
assume x in dom v1 ; :: thesis:
then reconsider j = x as Element of dom X by A2, A5, DCARXX;

per cases ;

suppose j = i ; :: thesis:

hence v1 . x = ((reproj (i,v0)) . (v1 . i)) . x by LOPBAN10:15; :: thesis:

end;

suppose A8: j <> i ; :: thesis:

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:

end;

then A10: v1 = (reproj (i,v0)) . (v1 . i) by A2, A5, A6, FUNCT_1:2;
reconsider v3 = (reproj (i,v0)) . ((v1 . i) - (v0 . i)) as Point of (product X) ;
(f /. v1) - (f /. v0) = (f . ((reproj (i,v0)) . (v1 . i))) - (f . ((reproj (i,v0)) . (v0 . i))) by A10, LOPBAN10:17
.= ((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 A3, LOPBAN_1:def 5
.= (f * (reproj (i,v0))) . ((v1 . i) + ((- 1) * (v0 . i))) by A3, VECTSP_1:def 20
.= (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 * (NrProduct v3) 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 A13, FINSEQ_1:def 3;
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 A14, LM03;
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 A19, FINSEQ_1:def 3;
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:
assume k in dom Nx ; :: thesis:
then A22: k in Seg (len Nx) by FINSEQ_1:def 3;
then reconsider j = k as Element of dom X by A20, FINSEQ_1:def 3;
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 A20, A22, FUNCOP_1:7 ;

now :: thesis:

per cases ;

suppose A27: j = i ; :: thesis:

v3 . j = (v1 . i) - (v0 . i) by A27, LOPBAN10:15
.= (v1 - v0) . i by LOPBAN10:26 ;
then A29: Nx . k = ||.((v1 - v0) . i).|| by A19, A27;
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 A13, A20, A22, A26, A27, A29, FUNCT_7:31; :: thesis:

end;

suppose A30: j <> i ; :: thesis:

then A31: R2 . k = R1 . j by FUNCT_7:32
.= 1 by A20, A22, FUNCOP_1:7 ;
||.(v0 . j).|| <= ||.v0.|| by A4, PRVECT_2:10;
then ||.(v0 . j).|| + 0 <= ||.v0.|| + 1 by XREAL_1:7;
hence Nx . k <= (mlt (R2,R3)) . k by A24, A26, A30, A31, LOPBAN10:16; :: thesis:

end;

hence ( Nx . k <= (mlt (R2,R3)) . k & 0 <= Nx . k ) by A24; :: thesis:

end;

then NrProduct v3 <= ||.((v1 - v0) . i).|| * ((||.v0.|| + 1) |^ (len X)) by A16, A17, A18, A19, A20, A21, FINSEQ_9:34;
then K * (NrProduct v3) <= K * (((||.v0.|| + 1) |^ (len X)) * ||.((v1 - v0) . i).||) by A1, XREAL_1:66;
hence ||.((f /. v1) - (f /. v0)).|| <= (((||.v0.|| + 1) |^ (len X)) * K) * ||.((v1 - v0) . i).|| by A12, XXREAL_0:2; :: thesis: