defpred S_{1}[ Real, set ] means $2 = r * $1;

A1: for x being Element of I[01] ex y being Element of the carrier of R^1 st S_{1}[x,y]

for x being Element of I[01] holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A1);

hence ex b_{1} being Function of I[01],R^1 st

for x being Point of I[01] holds b_{1} . x = r * x
; :: thesis: verum

A1: for x being Element of I[01] ex y being Element of the carrier of R^1 st S

proof

ex f being Function of the carrier of I[01], the carrier of R^1 st
let x be Element of I[01]; :: thesis: ex y being Element of the carrier of R^1 st S_{1}[x,y]

take r * x ; :: thesis: ( r * x is Element of the carrier of R^1 & S_{1}[x,r * x] )

thus ( r * x is Element of the carrier of R^1 & S_{1}[x,r * x] )
by TOPMETR:17, XREAL_0:def 1; :: thesis: verum

end;take r * x ; :: thesis: ( r * x is Element of the carrier of R^1 & S

thus ( r * x is Element of the carrier of R^1 & S

for x being Element of I[01] holds S

hence ex b

for x being Point of I[01] holds b