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.]

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

for x being set st x in [:(R^1 [.0,1.]),(R^1 [.0,1.]):] holds

f . x in R^1 [.0,1.]

proof

then reconsider A = R^1 [.0,1.] as Preserv of f by REALSET1:def 1;
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;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

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