let f be LinearOperator of m,n; :: thesis: f is bounded
A1: ( m in NAT & n in NAT ) by ORDINAL1:def 12;
defpred S₁[ Nat, set ] 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] ;
consider KS being FinSequence of REAL such that
A3: ( 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

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 A3;
hence 0 <= KS . j ; :: thesis: verum

end;

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

now

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

A6: now

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 A5, 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
A7: ( dom fx = Seg m & ( for i being Nat st i in Seg m holds
S₂[i,fx . i] ) ) from FINSEQ_1:sch 5(A6);
A8: ( x = Sum (ProjFinSeq x) & len fx = m ) by A1, A7, EUCLID_7:31, FINSEQ_1:def 3;

now

let i be Element of 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 A5, FINSEQ_1:def 3;
hence fx . i = f . ((ProjFinSeq x) . i) by A7; :: thesis: verum

end;

then A9: Sum fx = f . x by A1, A5, A8, Th16;
reconsider x0 = x as Element of REAL m ;
A10: 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 A11: ( 1 <= i & i <= m ) ; :: thesis: ex v being Element of REAL n st
( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| )
then A12: (ProjFinSeq x) . i = |(x,(Base_FinSeq (m,i)))| * (Base_FinSeq (m,i)) by EUCLID_7:def 12;
A13: i in Seg m by A11, FINSEQ_1:1;
then reconsider v = fx . i as Element of REAL n by A7, PARTFUN1:4;
take v ; :: thesis: ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq (m,i))).| )
v = f . ((ProjFinSeq x) . i) by A7, A13;
then v = |(x,(Base_FinSeq (m,i)))| * (f . (Base_FinSeq (m,i))) by A12, Def2;
then v = (x0 . i) * (f . (Base_FinSeq (m,i))) by A11, 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 A13, 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.| );

A14: now

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 A7, PARTFUN1:4;
|.v.| in REAL ;
hence ex x being Element of REAL st S₃[k,x] ; :: thesis: verum

end;

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

A19: now

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

end;

A22: zfx is Element of m -tuples_on REAL by A16, FINSEQ_2:92;
len KS = m by A1, A3, 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 A19, A22, RVSUM_1:82;
then Sum zfx <= |.x.| * (Sum KS) by RVSUM_1:87;
then A23: |.(f . x).| <= |.x.| * (Sum KS) by A18, 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 A23, XXREAL_0:2; :: thesis: verum

end;

hence f is bounded by A4, Def3; :: thesis: verum