defpred S₁[ object , Element of REAL ] means ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( y = $1 & z = y |-- b & $2 = (max_norm (dim X)) . z );
A1: for x being Element of the carrier of X ex r being Element of REAL st S₁[x,r]

let x be Element of the carrier of X; :: thesis:
reconsider y = x as Element of (RLSp2RVSp X) ;
reconsider z = y |-- b as Element of REAL (dim X) by Th17;
reconsider r = (max_norm (dim X)) . z as Element of REAL ;
take r ; :: thesis:
thus S₁[x,r] ; :: thesis:

end;

consider w being Function of the carrier of X,REAL such that
A2: for x being Element of the carrier of X holds S₁[x,w . x] from FUNCT_2:sch 3(A1);
take w ; :: thesis:
thus for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & w . x = (max_norm (dim X)) . z ) by A2; :: thesis: