defpred S₁[ real number , 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₁[x,y]

proof

let x be Element of I[01]; :: thesis: ex y being Element of the carrier of R^1 st S₁[x,y]
take r * x ; :: thesis: ( r * x is Element of the carrier of R^1 & S₁[x,r * x] )
thus ( r * x is Element of the carrier of R^1 & S₁[x,r * x] ) by TOPMETR:17, XREAL_0:def 1; :: thesis: verum

end;

ex f being Function of the carrier of I[01], the carrier of R^1 st
for x being Element of I[01] holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
hence ex b₁ being Function of I[01],R^1 st
for x being Point of I[01] holds b₁ . x = r * x ; :: thesis: verum