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 ;
( 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.]):]
;
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;
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; verum