deffunc H1( Element of (TOP-REAL 1), Element of the carrier of I[01]) -> Element of the carrier of (TOP-REAL 1) = (1 - $2) * $1;
consider G being Function of [: the carrier of (TOP-REAL 1), the carrier of I[01]:], the carrier of (TOP-REAL 1) such that
A1:
for x being Point of (TOP-REAL 1)
for i being Point of I[01] holds G . (x,i) = H1(x,i)
from BINOP_1:sch 4();
reconsider G = G as Function of [:(TOP-REAL 1),I[01]:],(TOP-REAL 1) by Lm2;
consider f being Function of (TOP-REAL 1),R^1 such that
A2:
for p being Element of (TOP-REAL 1) holds f . p = p /. 1
by JORDAN2B:1;
A3:
f is being_homeomorphism
by A2, JORDAN2B:28;
then A4:
f is continuous
by TOPS_2:def 5;
let F be Function of [:R^1,I[01]:],R^1; ( ( for x being Point of R^1
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) implies F is continuous )
assume A5:
for x being Point of R^1
for i being Point of I[01] holds F . (x,i) = (1 - i) * x
; F is continuous
A6:
for x being Point of [:R^1,I[01]:] holds F . x = (f * (G * [:(f "),(id I[01]):])) . x
proof
reconsider ff =
f as
Function ;
let x be
Point of
[:R^1,I[01]:];
F . x = (f * (G * [:(f "),(id I[01]):])) . x
consider a being
Point of
R^1,
b being
Point of
I[01] such that A7:
x = [a,b]
by BORSUK_1:10;
A8:
dom (f ") = the
carrier of
R^1
by FUNCT_2:def 1;
rng f = [#] R^1
by A3, TOPS_2:def 5;
then A9:
f is
onto
by FUNCT_2:def 3;
A10:
dom f = the
carrier of
(TOP-REAL 1)
by FUNCT_2:def 1;
set g =
ff " ;
consider z being
Real such that A11:
(1 - b) * ((f ") . a) = <*z*>
by JORDAN2B:20;
reconsider zz =
z as
Element of
REAL by XREAL_0:def 1;
A12:
<*a*> = |[a]|
;
then reconsider w =
<*a*> as
Element of
REAL 1
by EUCLID:22;
A13:
ff is
one-to-one
by A3, TOPS_2:def 5;
f . <*a*> =
|[a]| /. 1
by A2
.=
a
by Th4
;
then
<*a*> = (ff ") . a
by A10, A13, A12, FUNCT_1:32;
then A14:
w = (f /") . a
by A9, A13, TOPS_2:def 4;
A15:
<*z*> =
(1 - b) * ((f /") . a)
by A11
.=
(1 - b) * w
by A14
.=
<*((1 - b) * a)*>
by RVSUM_1:47
;
thus (f * (G * [:(f "),(id I[01]):])) . x =
f . ((G * [:(f "),(id I[01]):]) . x)
by FUNCT_2:15
.=
f . (G . ([:(f "),(id I[01]):] . (a,b)))
by A7, FUNCT_2:15
.=
f . (G . (((f ") . a),((id I[01]) . b)))
by A8, Lm4, FUNCT_3:def 8
.=
f . (G . (((f ") . a),b))
by FUNCT_1:18
.=
f . ((1 - b) * ((f ") . a))
by A1
.=
((1 - b) * ((f ") . a)) /. 1
by A2
.=
<*zz*> /. 1
by A11
.=
z
by FINSEQ_4:16
.=
(1 - b) * a
by A15, FINSEQ_1:76
.=
F . (
a,
b)
by A5
.=
F . x
by A7
;
verum
end;
f " is continuous
by A3, TOPS_2:def 5;
then A16:
[:(f "),(id I[01]):] is continuous
;
G is continuous
by A1, TOPALG_1:17;
hence
F is continuous
by A4, A16, A6, FUNCT_2:63; verum