let f be LinearOperator of m,n; :: thesis: f is Lipschitzian
A1: ( m in NAT & n in NAT ) by ORDINAL1:def 12;
defpred S₁[ Nat, object ] means n = |.(f . (Base_FinSeq (m,m))).|;
A2: for k0 being Nat st k0 in Seg m holds
ex v being Element of REAL st S₁[k0,v]

proof

let k0 be Nat; :: thesis: ( k0 in Seg m implies ex v being Element of REAL st S₁[k0,v] )
assume k0 in Seg m ; :: thesis: ex v being Element of REAL st S₁[k0,v]
consider v being Real such that
A3: S₁[k0,v] ;
reconsider v = v as Element of REAL by XREAL_0:def 1;
S₁[k0,v] by A3;
hence ex v being Element of REAL st S₁[k0,v] ; :: thesis: verum

end;

consider KS being FinSequence of REAL such that
A4: ( dom KS = Seg m & ( for i being Nat st i in Seg m holds
S₁[i,KS . i] ) ) from FINSEQ_1:sch 5(A2);
set K = (Sum KS) + 1;

now :: thesis: for j being Nat st j in dom KS holds
0 <= KS . j

let j be Nat; :: thesis: ( j in dom KS implies 0 <= KS . j )
assume j in dom KS ; :: thesis: 0 <= KS . j
then KS . j = |.(f . (Base_FinSeq (m,j))).| by A4;
hence 0 <= KS . j ; :: thesis: verum

end;

then A5: 0 <= Sum KS by RVSUM_1:84;
reconsider m0 = m as Nat ;

now :: thesis: for x being Element of REAL m holds |.(f . x).| <= ((Sum KS) + 1) * |.x.|

let x be Element of REAL m; :: thesis: |.(f . x).| <= ((Sum KS) + 1) * |.x.|
A6: len (ProjFinSeq x) = m by EUCLID_7:def 12;
defpred S₂[ set , set ] means n = f . ((ProjFinSeq x) . m);

A7: now :: thesis: for k being Nat st k in Seg m holds
ex x being Element of REAL n st S₂[k,x]

let k be Nat; :: thesis: ( k in Seg m implies ex x being Element of REAL n st S₂[k,x] )
assume k in Seg m ; :: thesis: ex x being Element of REAL n st S₂[k,x]
then k in dom (ProjFinSeq x) by A6, FINSEQ_1:def 3;
then reconsider v = (ProjFinSeq x) . k as Element of REAL m by PARTFUN1:4;
f . v is Element of REAL n ;
hence ex x being Element of REAL n st S₂[k,x] ; :: thesis: verum

end;

consider fx being FinSequence of REAL n such that
A8: ( dom fx = Seg m & ( for i being Nat st i in Seg m holds
S₂[i,fx . i] ) ) from FINSEQ_1:sch 5(A7);
A9: ( x = Sum (ProjFinSeq x) & len fx = m ) by A1, A8, EUCLID_7:31, FINSEQ_1:def 3;

now :: thesis: for i being Nat st i in dom (ProjFinSeq x) holds
fx . i = f . ((ProjFinSeq x) . i)

let i be Nat; :: thesis: ( i in dom (ProjFinSeq x) implies fx . i = f . ((ProjFinSeq x) . i) )
assume i in dom (ProjFinSeq x) ; :: thesis: fx . i = f . ((ProjFinSeq x) . i)
then i in Seg m by A6, FINSEQ_1:def 3;
hence fx . i = f . ((ProjFinSeq x) . i) by A8; :: thesis: verum

end;

then A10: Sum fx = f . x by A6, A9, Th16;
reconsider x0 = x as Element of REAL m ;
A11: for i being Nat st 1 <= i & i <= m holds
ex v being Element of REAL n st
( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| )

proof

let i be Nat; :: thesis: ( 1 <= i & i <= m implies ex v being Element of REAL n st
( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| ) )
assume A12: ( 1 <= i & i <= m ) ; :: thesis: ex v being Element of REAL n st
( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| )
then A13: (ProjFinSeq x) . i = |(x,(Base_FinSeq (m,i)))| * (Base_FinSeq (m,i)) by EUCLID_7:def 12;
A14: i in Seg m by A12;
then reconsider v = fx . i as Element of REAL n by A8, PARTFUN1:4;
take v ; :: thesis: ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| )
v = f . ((ProjFinSeq x) . i) by A8, A14;
then v = |(x,(Base_FinSeq (m,i)))| * (f . (Base_FinSeq (m,i))) by A13, Def2;
then v = (x0 . i) * (f . (Base_FinSeq (m,i))) by A12, EUCLID_7:30;
then |.v.| = |.(x0 . i).| * |.(f . (Base_FinSeq (m,i))).| by EUCLID:11;
hence ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| ) by A14, REAL_NS1:8, XREAL_1:64; :: thesis: verum

end;

defpred S₃[ set , set ] means ex v being Element of REAL n st
( v = fx . m & n = |.v.| );

A15: now :: thesis: for k being Nat st k in Seg m holds
ex x being Element of REAL st S₃[k,x]

let k be Nat; :: thesis: ( k in Seg m implies ex x being Element of REAL st S₃[k,x] )
assume k in Seg m ; :: thesis: ex x being Element of REAL st S₃[k,x]
then reconsider v = fx . k as Element of REAL n by A8, PARTFUN1:4;
|.v.| in REAL by XREAL_0:def 1;
hence ex x being Element of REAL st S₃[k,x] ; :: thesis: verum

end;

consider zfx being FinSequence of REAL such that
A16: ( dom zfx = Seg m & ( for i being Nat st i in Seg m holds
S₃[i,zfx . i] ) ) from FINSEQ_1:sch 5(A15);
A17: len zfx = m by A1, A16, FINSEQ_1:def 3;
then A18: len fx = len zfx by A8, FINSEQ_1:def 3;
for i being Nat st i in dom fx holds
ex v being Element of REAL n st
( v = fx . i & zfx . i = |.v.| ) by A8, A16;
then A19: |.(f . x).| <= Sum zfx by A10, A18, Th17;

A20: now :: thesis: for j being Nat st j in Seg m holds
zfx . j <= (|.x.| * KS) . j

let j be Nat; :: thesis: ( j in Seg m implies zfx . j <= (|.x.| * KS) . j )
assume A21: j in Seg m ; :: thesis: zfx . j <= (|.x.| * KS) . j
then A22: ex v being Element of REAL n st
( v = fx . j & zfx . j = |.v.| ) by A16;
( 1 <= j & j <= m ) by A21, FINSEQ_1:1;
then ex v being Element of REAL n st
( v = fx . j & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,j))).| ) by A11;
then zfx . j <= |.x.| * (KS . j) by A4, A21, A22;
hence zfx . j <= (|.x.| * KS) . j by VALUED_1:6; :: thesis: verum

end;

A23: zfx is Element of m -tuples_on REAL by A17, FINSEQ_2:92;
len KS = m by A1, A4, FINSEQ_1:def 3;
then reconsider KS0 = KS as Element of REAL m0 by FINSEQ_2:92;
|.x.| * KS0 is Element of m0 -tuples_on REAL ;
then Sum zfx <= Sum (|.x.| * KS) by A20, A23, RVSUM_1:82;
then Sum zfx <= |.x.| * (Sum KS) by RVSUM_1:87;
then A24: |.(f . x).| <= |.x.| * (Sum KS) by A19, XXREAL_0:2;
0 + (Sum KS) <= 1 + (Sum KS) by XREAL_1:6;
then |.x.| * (Sum KS) <= |.x.| * (1 + (Sum KS)) by XREAL_1:64;
hence |.(f . x).| <= ((Sum KS) + 1) * |.x.| by A24, XXREAL_0:2; :: thesis: verum

end;

hence f is Lipschitzian by A5; :: thesis: verum