defpred S₁[ object , Element of REAL ] means ex x being Element of REAL n st
( x = $1 & $2 = Sum (abs x) );
A1: 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]
reconsider y = Sum (abs x) as Element of REAL ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider w being Function of (REAL n),REAL such that
A2: for x being Element of REAL n holds S₁[x,w . x] from FUNCT_2:sch 3(A1);
take w ; :: thesis: for x being Element of REAL n holds w . x = Sum (abs x)
thus for x being Element of REAL n holds w . x = Sum (abs x) :: thesis: verum

proof

let x be Element of REAL n; :: thesis: w . x = Sum (abs x)
ex x0 being Element of REAL n st
( x0 = x & w . x = Sum (abs x0) ) by A2;
hence w . x = Sum (abs x) ; :: thesis: verum

end;