let f be LinearOperator of m,n; :: thesis: f is bounded
A0: ( m in NAT & n in NAT ) by ORDINAL1:def 13;
defpred S₁[ Nat, set ] means n = |.(f . (Base_FinSeq m,m)).|;
A1: 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
A2: ( dom KS = Seg m & ( for i being Nat st i in Seg m holds
S₁[i,KS . i] ) ) from FINSEQ_1:sch 5(A1);
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 A2;
hence 0 <= KS . j ; :: thesis: verum

end;

then A3: 0 <= Sum KS by RVSUM_1:114;
reconsider m0 = m as Nat ;

now

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

A5: 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 A4, FINSEQ_1:def 3;
then reconsider v = (ProjFinSeq x) . k as Element of REAL m by PARTFUN1:27;
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
A6: ( dom fx = Seg m & ( for i being Nat st i in Seg m holds
S₂[i,fx . i] ) ) from FINSEQ_1:sch 5(A5);
A7: ( x = Sum (ProjFinSeq x) & len fx = m ) by A0, A6, EUCLID_7:33, 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 A4, FINSEQ_1:def 3;
hence fx . i = f . ((ProjFinSeq x) . i) by A6; :: thesis: verum

end;

then A8: Sum fx = f . x by A0, A4, A7, LOPBTh255;
reconsider x0 = x as Element of REAL m ;
A9: 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 A10: ( 1 <= i & i <= m ) ; :: thesis: ex v being Element of REAL n st
( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq m,i)).| )
then A11: (ProjFinSeq x) . i = |(x,(Base_FinSeq m,i))| * (Base_FinSeq m,i) by EUCLID_7:def 12;
A12: i in Seg m by A10, FINSEQ_1:3;
then reconsider v = fx . i as Element of REAL n by A6, PARTFUN1:27;
take v ; :: thesis: ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq m,i)).| )
v = f . ((ProjFinSeq x) . i) by A6, A12;
then v = |(x,(Base_FinSeq m,i))| * (f . (Base_FinSeq m,i)) by A11, LOPBDef6;
then v = (x0 . i) * (f . (Base_FinSeq m,i)) by A10, EUCLID_7:32;
then |.v.| = |.(x0 . i).| * |.(f . (Base_FinSeq m,i)).| by EUCLID:14;
hence ( v = fx . i & |.v.| <= |.x.| * |.(f . (Base_FinSeq m,i)).| ) by A0, A12, REAL_NS1:8, XREAL_1:66; :: thesis: verum

end;

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

A13: 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 A6, PARTFUN1:27;
|.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
A14: ( dom zfx = Seg m & ( for i being Nat st i in Seg m holds
S₃[i,zfx . i] ) ) from FINSEQ_1:sch 5(A13);
A15: len zfx = m by A0, A14, FINSEQ_1:def 3;
then A16: len fx = len zfx by A6, 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 A6, A14;
then A17: |.(f . x).| <= Sum zfx by A0, A8, A16, LOPBTh258;

A18: now

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

end;

A21: zfx is Element of m -tuples_on REAL by A15, FINSEQ_2:110;
len KS = m by A0, A2, FINSEQ_1:def 3;
then reconsider KS0 = KS as Element of REAL m0 by FINSEQ_2:110;
|.x.| * KS0 is Element of m0 -tuples_on REAL ;
then Sum zfx <= Sum (|.x.| * KS) by A18, A21, RVSUM_1:112;
then Sum zfx <= |.x.| * (Sum KS) by RVSUM_1:117;
then A22: |.(f . x).| <= |.x.| * (Sum KS) by A17, XXREAL_0:2;
0 + (Sum KS) <= 1 + (Sum KS) by XREAL_1:8;
then |.x.| * (Sum KS) <= |.x.| * (1 + (Sum KS)) by XREAL_1:66;
hence |.(f . x).| <= ((Sum KS) + 1) * |.x.| by A22, XXREAL_0:2; :: thesis: verum

end;

hence f is bounded by A3, LOPBDef9; :: thesis: verum