defpred S₁[ object , Element of REAL ] means ex x being Element of REAL n st
( x = $1 & $2 in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= $2 ) );
A2: for x being Element of REAL n ex y being Element of REAL st S₁[x,y]

proof

let x be Element of REAL n; :: thesis: ex y being Element of REAL st S₁[x,y]
consider xMAX being Real such that
A3: ( xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) ) by A1, Th8;
reconsider xMAX = xMAX as Element of REAL by XREAL_0:def 1;
take xMAX ; :: thesis: S₁[x,xMAX]
thus S₁[x,xMAX] by A3; :: thesis: verum

end;

consider w being Function of (REAL n),REAL such that
A4: for x being Element of REAL n holds S₁[x,w . x] from FUNCT_2:sch 3(A2);
take w ; :: thesis: for x being Element of REAL n holds
( w . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= w . x ) )
thus for x being Element of REAL n holds
( w . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= w . x ) ) :: thesis: verum

proof

let x be Element of REAL n; :: thesis: ( w . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= w . x ) )
ex x0 being Element of REAL n st
( x0 = x & w . x in rng (abs x0) & ( for i being Nat st i in dom x0 holds
(abs x0) . i <= w . x ) ) by A4;
hence ( w . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= w . x ) ) ; :: thesis: verum

end;