let n be non empty Nat; :: thesis: for x being Element of REAL n ex xMAX being Real st
( xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) )
let x be Element of REAL n; :: thesis: ex xMAX being Real st
( xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) )
set F = rng (abs x);
A1: ( rng (abs x) is bounded_above & upper_bound (rng (abs x)) in rng (abs x) ) by SEQ_4:133;
set xMAX = upper_bound (rng (abs x));
reconsider xMAX = upper_bound (rng (abs x)) as Real ;
take xMAX ; :: thesis: ( xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) )
thus xMAX in rng (abs x) by SEQ_4:133; :: thesis: for i being Nat st i in dom x holds
(abs x) . i <= xMAX
thus for i being Nat st i in dom x holds
(abs x) . i <= xMAX :: thesis: verum
proof
let i be Nat; :: thesis: ( i in dom x implies (abs x) . i <= xMAX )
assume i in dom x ; :: thesis: (abs x) . i <= xMAX
then i in dom (abs x) by VALUED_1:def 11;
then (abs x) . i in rng (abs x) by FUNCT_1:3;
hence (abs x) . i <= xMAX by A1, SEQ_4:def 1; :: thesis: verum
end;