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 )

proof

assume A2: f is bounded ; :: thesis: g is bounded
defpred S₁[ 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₁[i,di]

proof

let i be Nat; :: thesis: ( i in Seg n implies ex di being Element of REAL st S₁[i,di] )
set P = proj (i,n);
assume i in Seg n ; :: thesis: ex di being Element of REAL st S₁[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₁[i,r]
thus S₁[i,r] by A4; :: thesis: verum

end;

consider d being FinSequence of REAL such that
A5: ( dom d = Seg n & ( for k being Nat st k in Seg n holds
S₁[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

proof

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;

now :: thesis: for i being Element of NAT st 1 <= i & i <= n holds
|.((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;

then A12: |.(f /. y).| < (n * (max d)) + 1 by PDIFF_8:15, XREAL_1:145;
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;

hence g is bounded ; :: thesis: verum

end;

assume A13: g is bounded ; :: thesis: 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

proof

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;

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