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 )

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

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
|.f.| is bounded
; :: thesis: f is bounded assume A1:
f is bounded
; :: thesis: |.f.| is bounded

defpred S_{1}[ 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_{1}[i,r]

A6: ( dom w = Seg n & ( for i being Nat st i in Seg n holds

S_{1}[i,w . i] ) )
from FINSEQ_1:sch 5(A2);

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

end;defpred S

( 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

proof

consider w being FinSequence of REAL such that
let i be Nat; :: thesis: ( i in Seg n implies ex r being Element of REAL st S_{1}[i,r] )

assume A3: i in Seg n ; :: thesis: ex r being Element of REAL st S_{1}[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_{1}[i,r]

_{1}[i,r]
by COMPLEX1:46; :: thesis: verum

end;assume A3: i in Seg n ; :: thesis: ex r being Element of REAL st S

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

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

|.(((proj (i,n)) * f) . y).| < r

hence
S|.(((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;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

A6: ( dom w = Seg n & ( for i being Nat st i in Seg n holds

S

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 ) )

len w = n
by A6, FINSEQ_1:def 3;( 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_{1}[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;|.(((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

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

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

hence
|.f.| is bounded
by COMSEQ_2:def 3; :: thesis: verum
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;

then 0 + |.(|.f.| . y).| < (n * (Sum w)) + 1 by A10, A11, XREAL_1:8;

hence |.(|.f.| . y).| < (n * (Sum w)) + 1 ; :: thesis: verum

end;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

then
|.(f /. y).| <= n * (Sum w)
by PDIFF_8:17;|.((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;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

then 0 + |.(|.f.| . y).| < (n * (Sum w)) + 1 by A10, A11, XREAL_1:8;

hence |.(|.f.| . y).| < (n * (Sum w)) + 1 ; :: thesis: verum

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

hence
(proj (i,n)) * f is bounded
by COMSEQ_2:def 3; :: thesis: verum
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;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