let n be Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n)

for g being PartFunc of REAL,(REAL-NS n) st f = g holds

( f is bounded iff g is bounded )

let f be PartFunc of REAL,(REAL n); :: thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g holds

( f is bounded iff g is bounded )

let g be PartFunc of REAL,(REAL-NS n); :: thesis: ( f = g implies ( f is bounded iff g is bounded ) )

assume A1: f = g ; :: thesis: ( f is bounded iff g is bounded )

thus ( f is bounded implies g is bounded ) :: thesis: ( g is bounded implies f is bounded )

consider r being Real such that

A14: for y being set st y in dom g holds

||.(g /. y).|| < r by A13;

let i be Element of NAT ; :: according to INTEGR15:def 15 :: thesis: ( not i in Seg n or (proj (i,n)) * f is bounded )

set P = proj (i,n);

assume A15: 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).| < r

for g being PartFunc of REAL,(REAL-NS n) st f = g holds

( f is bounded iff g is bounded )

let f be PartFunc of REAL,(REAL n); :: thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g holds

( f is bounded iff g is bounded )

let g be PartFunc of REAL,(REAL-NS n); :: thesis: ( f = g implies ( f is bounded iff g is bounded ) )

assume A1: f = g ; :: thesis: ( f is bounded iff g is bounded )

thus ( f is bounded implies g is bounded ) :: thesis: ( g is bounded implies f is bounded )

proof

assume A13:
g is bounded
; :: thesis: f is bounded
assume A2:
f is bounded
; :: thesis: g is bounded

defpred S_{1}[ Nat, Element of REAL ] means for y being set st y in dom ((proj ($1,n)) * f) holds

|.(((proj ($1,n)) * f) . y).| < $2;

A3: for i being Nat st i in Seg n holds

ex di being Element of REAL st S_{1}[i,di]

A5: ( dom d = Seg n & ( for k being Nat st k in Seg n holds

S_{1}[k,d /. k] ) )
from RECDEF_1:sch 17(A3);

set K = max d;

for y being set st y in dom g holds

||.(g /. y).|| < (n * (max d)) + 1

end;defpred S

|.(((proj ($1,n)) * f) . y).| < $2;

A3: for i being Nat st i in Seg n holds

ex di being Element of REAL st S

proof

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

set P = proj (i,n);

assume i in Seg n ; :: thesis: ex di being Element of REAL st S_{1}[i,di]

then (proj (i,n)) * f is bounded by A2;

then consider r being Real such that

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

|.(((proj (i,n)) * f) . y).| < r by COMSEQ_2:def 3;

reconsider r = r as Element of REAL by XREAL_0:def 1;

take r ; :: thesis: S_{1}[i,r]

thus S_{1}[i,r]
by A4; :: thesis: verum

end;set P = proj (i,n);

assume i in Seg n ; :: thesis: ex di being Element of REAL st S

then (proj (i,n)) * f is bounded by A2;

then consider r being Real such that

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

|.(((proj (i,n)) * f) . y).| < r by COMSEQ_2:def 3;

reconsider r = r as Element of REAL by XREAL_0:def 1;

take r ; :: thesis: S

thus S

A5: ( dom d = Seg n & ( for k being Nat st k in Seg n holds

S

set K = max d;

for y being set st y in dom g holds

||.(g /. y).|| < (n * (max d)) + 1

proof

hence
g is bounded
; :: thesis: verum
let y be set ; :: thesis: ( y in dom g implies ||.(g /. y).|| < (n * (max d)) + 1 )

assume A6: y in dom g ; :: thesis: ||.(g /. y).|| < (n * (max d)) + 1

set s = f /. y;

g /. y = g . y by A6, PARTFUN1:def 6

.= f /. y by A1, A6, PARTFUN1:def 6 ;

hence ||.(g /. y).|| < (n * (max d)) + 1 by A12, REAL_NS1:1; :: thesis: verum

end;assume A6: y in dom g ; :: thesis: ||.(g /. y).|| < (n * (max d)) + 1

set s = f /. y;

now :: thesis: for i being Element of NAT st 1 <= i & i <= n holds

|.((f /. y) . i).| <= max d

then A12:
|.(f /. y).| < (n * (max d)) + 1
by PDIFF_8:15, XREAL_1:145;|.((f /. y) . i).| <= max d

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies |.((f /. y) . i).| <= max d )

set P = proj (i,n);

assume A7: ( 1 <= i & i <= n ) ; :: thesis: |.((f /. y) . i).| <= max d

then A8: i in Seg n ;

dom (proj (i,n)) = REAL n by FUNCT_2:def 1;

then rng f c= dom (proj (i,n)) ;

then A9: y in dom ((proj (i,n)) * f) by A6, A1, RELAT_1:27;

then A10: |.(((proj (i,n)) * f) . y).| < d /. i by A8, A5;

f . y = f /. y by A6, A1, PARTFUN1:def 6;

then ((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y) by A9, FUNCT_1:12;

then A11: |.((f /. y) . i).| < d /. i by A10, PDIFF_1:def 1;

len d = n by A5, FINSEQ_1:def 3;

then d . i <= max d by A7, RFINSEQ2:1;

then d /. i <= max d by A8, A5, PARTFUN1:def 6;

hence |.((f /. y) . i).| <= max d by A11, XXREAL_0:2; :: thesis: verum

end;set P = proj (i,n);

assume A7: ( 1 <= i & i <= n ) ; :: thesis: |.((f /. y) . i).| <= max d

then A8: i in Seg n ;

dom (proj (i,n)) = REAL n by FUNCT_2:def 1;

then rng f c= dom (proj (i,n)) ;

then A9: y in dom ((proj (i,n)) * f) by A6, A1, RELAT_1:27;

then A10: |.(((proj (i,n)) * f) . y).| < d /. i by A8, A5;

f . y = f /. y by A6, A1, PARTFUN1:def 6;

then ((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y) by A9, FUNCT_1:12;

then A11: |.((f /. y) . i).| < d /. i by A10, PDIFF_1:def 1;

len d = n by A5, FINSEQ_1:def 3;

then d . i <= max d by A7, RFINSEQ2:1;

then d /. i <= max d by A8, A5, PARTFUN1:def 6;

hence |.((f /. y) . i).| <= max d by A11, XXREAL_0:2; :: thesis: verum

g /. y = g . y by A6, PARTFUN1:def 6

.= f /. y by A1, A6, PARTFUN1:def 6 ;

hence ||.(g /. y).|| < (n * (max d)) + 1 by A12, REAL_NS1:1; :: thesis: verum

consider r being Real such that

A14: for y being set st y in dom g holds

||.(g /. y).|| < r by A13;

let i be Element of NAT ; :: according to INTEGR15:def 15 :: thesis: ( not i in Seg n or (proj (i,n)) * f is bounded )

set P = proj (i,n);

assume A15: 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).| < r

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

assume A16: y in dom ((proj (i,n)) * f) ; :: thesis: |.(((proj (i,n)) * f) . y).| < r

dom (proj (i,n)) = REAL n by FUNCT_2:def 1;

then rng f c= dom (proj (i,n)) ;

then A17: y in dom f by A16, RELAT_1:27;

then A18: ||.(g /. y).|| < r by A14, A1;

set s = f /. y;

g /. y = g . y by A17, A1, PARTFUN1:def 6

.= f /. y by A1, A17, PARTFUN1:def 6 ;

then A19: |.(f /. y).| < r by A18, REAL_NS1:1;

|.((f /. y) . i).| <= |.(f /. y).| by A15, REAL_NS1:8;

then A20: |.((f /. y) . i).| < r by A19, XXREAL_0:2;

f . y = f /. y by A17, PARTFUN1:def 6;

then ((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y) by A16, FUNCT_1:12;

hence |.(((proj (i,n)) * f) . y).| < r by A20, PDIFF_1:def 1; :: thesis: verum

end;assume A16: y in dom ((proj (i,n)) * f) ; :: thesis: |.(((proj (i,n)) * f) . y).| < r

dom (proj (i,n)) = REAL n by FUNCT_2:def 1;

then rng f c= dom (proj (i,n)) ;

then A17: y in dom f by A16, RELAT_1:27;

then A18: ||.(g /. y).|| < r by A14, A1;

set s = f /. y;

g /. y = g . y by A17, A1, PARTFUN1:def 6

.= f /. y by A1, A17, PARTFUN1:def 6 ;

then A19: |.(f /. y).| < r by A18, REAL_NS1:1;

|.((f /. y) . i).| <= |.(f /. y).| by A15, REAL_NS1:8;

then A20: |.((f /. y) . i).| < r by A19, XXREAL_0:2;

f . y = f /. y by A17, PARTFUN1:def 6;

then ((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y) by A16, FUNCT_1:12;

hence |.(((proj (i,n)) * f) . y).| < r by A20, PDIFF_1:def 1; :: thesis: verum