let A be non empty closed_interval Subset of REAL; :: thesis: for n being non zero Element of NAT
for f being Function of A,(REAL n) holds
( f is bounded iff |.f.| is bounded )
let n be non zero Element of NAT ; :: thesis: for f being Function of A,(REAL n) holds
( f is bounded iff |.f.| is bounded )
let f be Function of A,(REAL n); :: thesis: ( f is bounded iff |.f.| is bounded )

hereby :: thesis: ( |.f.| is bounded implies f is bounded )

assume A1: f is bounded ; :: thesis: |.f.| is bounded
defpred S₁[ Nat, set ] means ex K being Element of REAL st
( 0 <= K & K = $2 & ( for y being set st y in dom ((proj ($1,n)) * f) holds
|.(((proj ($1,n)) * f) . y).| < K ) );
A2: for i being Nat st i in Seg n holds
ex r being Element of REAL st S₁[i,r]

proof

let i be Nat; :: thesis: ( i in Seg n implies ex r being Element of REAL st S₁[i,r] )
assume A3: i in Seg n ; :: thesis: ex r being Element of REAL st S₁[i,r]
set P = proj (i,n);
(proj (i,n)) * f is bounded by A1, A3;
then consider L being Real such that
A4: for y being set st y in dom ((proj (i,n)) * f) holds
|.(((proj (i,n)) * f) . y).| < L by COMSEQ_2:def 3;
reconsider r = |.L.| as Element of REAL by XREAL_0:def 1;
take r ; :: thesis: S₁[i,r]

now :: thesis: for y being set st y in dom ((proj (i,n)) * f) holds
|.(((proj (i,n)) * f) . y).| < r

let y be set ; :: thesis: ( y in dom ((proj (i,n)) * f) implies |.(((proj (i,n)) * f) . y).| < r )
assume A5: y in dom ((proj (i,n)) * f) ; :: thesis: |.(((proj (i,n)) * f) . y).| < r
L <= r by ABSVALUE:4;
hence |.(((proj (i,n)) * f) . y).| < r by A4, A5, XXREAL_0:2; :: thesis: verum

end;

hence S₁[i,r] by COMPLEX1:46; :: thesis: verum

end;

consider w being FinSequence of REAL such that
A6: ( dom w = Seg n & ( for i being Nat st i in Seg n holds
S₁[i,w . i] ) ) from FINSEQ_1:sch 5(A2);

A7: now :: thesis: for i being Element of NAT st i in Seg n holds
( 0 <= w . i & ( for y being set st y in dom ((proj (i,n)) * f) holds
|.(((proj (i,n)) * f) . y).| < w . i ) )

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( 0 <= w . i & ( for y being set st y in dom ((proj (i,n)) * f) holds
|.(((proj (i,n)) * f) . y).| < w . i ) ) )
set P = proj (i,n);
assume i in Seg n ; :: thesis: ( 0 <= w . i & ( for y being set st y in dom ((proj (i,n)) * f) holds
|.(((proj (i,n)) * f) . y).| < w . i ) )
then S₁[i,w . i] by A6;
hence ( 0 <= w . i & ( for y being set st y in dom ((proj (i,n)) * f) holds
|.(((proj (i,n)) * f) . y).| < w . i ) ) ; :: thesis: verum

end;

len w = n by A6, FINSEQ_1:def 3;
then reconsider w = w as Element of REAL n by FINSEQ_2:92;
A8: for i being Nat st i in Seg n holds
0 <= w . i by A7;
set KK = Sum w;
for y being set st y in dom |.f.| holds
|.(|.f.| . y).| < (n * (Sum w)) + 1

proof

let y be set ; :: thesis: ( y in dom |.f.| implies |.(|.f.| . y).| < (n * (Sum w)) + 1 )
assume A9: y in dom |.f.| ; :: thesis: |.(|.f.| . y).| < (n * (Sum w)) + 1
then A10: |.f.| . y = |.f.| /. y by PARTFUN1:def 6
.= |.(f /. y).| by A9, NFCONT_4:def 2 ;
then A11: |.(|.f.| . y).| = |.f.| . y by ABSVALUE:def 1;

now :: thesis: for i being Element of NAT st 1 <= i & i <= n holds
|.((proj (i,n)) . (f /. y)).| <= Sum w

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies |.((proj (i,n)) . (f /. y)).| <= Sum w )
set P = proj (i,n);
assume A12: ( 1 <= i & i <= n ) ; :: thesis: |.((proj (i,n)) . (f /. y)).| <= Sum w
A13: y in dom f by A9, NFCONT_4:def 2;
then f . y in rng f by FUNCT_1:3;
then f . y in REAL n ;
then f . y in dom (proj (i,n)) by FUNCT_2:def 1;
then A14: y in dom ((proj (i,n)) * f) by A13, FUNCT_1:11;
A15: i in Seg n by A12;
then |.(((proj (i,n)) * f) . y).| < w . i by A7, A14;
then |.((proj (i,n)) . (f . y)).| < w . i by A14, FUNCT_1:12;
then A16: |.((proj (i,n)) . (f /. y)).| < w . i by A13, PARTFUN1:def 6;
w . i <= Sum w by A8, A15, REAL_NS1:7;
hence |.((proj (i,n)) . (f /. y)).| <= Sum w by A16, XXREAL_0:2; :: thesis: verum

end;

then |.(f /. y).| <= n * (Sum w) by PDIFF_8:17;
then 0 + |.(|.f.| . y).| < (n * (Sum w)) + 1 by A10, A11, XREAL_1:8;
hence |.(|.f.| . y).| < (n * (Sum w)) + 1 ; :: thesis: verum

end;

hence |.f.| is bounded by COMSEQ_2:def 3; :: thesis: verum

end;

assume |.f.| is bounded ; :: thesis: f is bounded
then consider K being Real such that
A17: for y being set st y in dom |.f.| holds
|.(|.f.| . y).| < K by COMSEQ_2:def 3;
let i be Element of NAT ; :: according to INTEGR15:def 12 :: thesis: ( not i in Seg n or (proj (i,n)) * f is bounded )
set P = proj (i,n);
assume A18: i in Seg n ; :: thesis: (proj (i,n)) * f is bounded
for y being set st y in dom ((proj (i,n)) * f) holds
|.(((proj (i,n)) * f) . y).| < K

proof

let y be set ; :: thesis: ( y in dom ((proj (i,n)) * f) implies |.(((proj (i,n)) * f) . y).| < K )
assume A19: y in dom ((proj (i,n)) * f) ; :: thesis: |.(((proj (i,n)) * f) . y).| < K
then A20: y in dom f by FUNCT_1:11;
A21: ((proj (i,n)) * f) . y = (proj (i,n)) . (f . y) by A19, FUNCT_1:12
.= (proj (i,n)) . (f /. y) by A20, PARTFUN1:def 6 ;
( 1 <= i & i <= n ) by A18, FINSEQ_1:1;
then A22: |.((proj (i,n)) . (f /. y)).| <= |.(f /. y).| by PDIFF_8:5;
A23: y in dom |.f.| by A20, NFCONT_4:def 2;
then |.(|.f.| . y).| < K by A17;
then |.(|.f.| /. y).| < K by A23, PARTFUN1:def 6;
then |.|.(f /. y).|.| < K by A23, NFCONT_4:def 2;
then |.(f /. y).| < K by ABSVALUE:def 1;
hence |.(((proj (i,n)) * f) . y).| < K by A21, A22, XXREAL_0:2; :: thesis: verum

end;

hence (proj (i,n)) * f is bounded by COMSEQ_2:def 3; :: thesis: verum