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 = |.z.| );
A1: for x being Element of the carrier of X ex r being Element of REAL st S₁[x,r]

proof

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

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: 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 = |.z.| )
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 = |.z.| ) by A2; :: thesis: verum