let n be Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,() 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,() st f = g holds
( f is bounded iff g is bounded )

let g be PartFunc of REAL,(); :: 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 S1[ 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 S1[i,di]
proof
let i be Nat; :: thesis: ( i in Seg n implies ex di being Element of REAL st S1[i,di] )
set P = proj (i,n);
assume i in Seg n ; :: thesis: ex di being Element of REAL st S1[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: S1[i,r]
thus S1[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
S1[k,d /. k] ) ) from 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 ;
then A10: |.(((proj (i,n)) * f) . y).| < d /. i by A8, A5;
f . y = f /. y by ;
then ((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y) by ;
then A11: |.((f /. y) . i).| < d /. i by ;
len d = n by ;
then d . i <= max d by ;
then d /. i <= max d by ;
hence |.((f /. y) . i).| <= max d by ; :: thesis: verum
end;
then A12: |.(f /. y).| < (n * (max d)) + 1 by ;
g /. y = g . y by
.= f /. y by ;
hence ||.(g /. y).|| < (n * (max d)) + 1 by ; :: 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 ;
then A18: ||.(g /. y).|| < r by ;
set s = f /. y;
g /. y = g . y by
.= f /. y by ;
then A19: |.(f /. y).| < r by ;
|.((f /. y) . i).| <= |.(f /. y).| by ;
then A20: |.((f /. y) . i).| < r by ;
f . y = f /. y by ;
then ((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y) by ;
hence |.(((proj (i,n)) * f) . y).| < r by ; :: thesis: verum
end;
hence (proj (i,n)) * f is bounded by COMSEQ_2:def 3; :: thesis: verum