reconsider f = R^1-TIMES as BinOp of the carrier of R^1 by Lm1;
for x being set st x in [:(R^1 [.0,1.]),(R^1 [.0,1.]):] holds
f . x in R^1 [.0,1.]

proof

let x be set ; :: thesis: ( x in [:(R^1 [.0,1.]),(R^1 [.0,1.]):] implies f . x in R^1 [.0,1.] )
assume x in [:(R^1 [.0,1.]),(R^1 [.0,1.]):] ; :: thesis: f . x in R^1 [.0,1.]
then consider a, b being object such that
A1: ( a in R^1 [.0,1.] & b in R^1 [.0,1.] ) and
A2: x = [a,b] by ZFMISC_1:def 2;
reconsider a = a, b = b as Point of I[01] by A1, BORSUK_1:40;
reconsider a1 = a, b1 = b as Point of R^1 by A1;
f . (a1,b1) = a * b by Def5;
hence f . x in R^1 [.0,1.] by A2, BORSUK_1:40; :: thesis: verum

end;

then reconsider A = R^1 [.0,1.] as Preserv of f by REALSET1:def 1;
A3: the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
f || A is BinOp of A ;
hence R^1-TIMES || (R^1 [.0,1.]) is Function of [:I[01],I[01]:],I[01] by A3, BORSUK_1:40; :: thesis: verum