defpred S1[ 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 S1[x,y]
proof
let x be Element of I[01]; :: thesis: ex y being Element of the carrier of R^1 st S1[x,y]
take r * x ; :: thesis: ( r * x is Element of the carrier of R^1 & S1[x,r * x] )
thus ( r * x is Element of the carrier of R^1 & S1[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 S1[x,f . x] from FUNCT_2:sch 3(A1);
 hence ex b1 being Function of I[01],R^1 st
for x being Point of I[01] holds b1 . x = r * x ; :: thesis: verum