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 S1[ 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 S1[i,r]
proof
let i be Nat; :: thesis: ( i in Seg n implies ex r being Element of REAL st S1[i,r] )
assume A3: i in Seg n ; :: thesis: ex r being Element of REAL st S1[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: S1[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 ; :: thesis: verum
end;
hence S1[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
S1[i,w . i] ) ) from
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 S1[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 ;
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 ;
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 ;
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 ;
A15: i in Seg n by A12;
then |.(((proj (i,n)) * f) . y).| < w . i by ;
then |.((proj (i,n)) . (f . y)).| < w . i by ;
then A16: |.((proj (i,n)) . (f /. y)).| < w . i by ;
w . i <= Sum w by ;
hence |.((proj (i,n)) . (f /. y)).| <= Sum w by ; :: thesis: verum
end;
then |.(f /. y).| <= n * (Sum w) by PDIFF_8:17;
then 0 + |.(|.f.| . y).| < (n * (Sum w)) + 1 by ;
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
.= (proj (i,n)) . (f /. y) by ;
( 1 <= i & i <= n ) by ;
then A22: |.((proj (i,n)) . (f /. y)).| <= |.(f /. y).| by PDIFF_8:5;
A23: y in dom |.f.| by ;
then |.(|.f.| . y).| < K by A17;
then |.(|.f.| /. y).| < K by ;
then |.|.(f /. y).|.| < K by ;
then |.(f /. y).| < K by ABSVALUE:def 1;
hence |.(((proj (i,n)) * f) . y).| < K by ; :: thesis: verum
end;
hence (proj (i,n)) * f is bounded by COMSEQ_2:def 3; :: thesis: verum