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:34;
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:50;
A8:
dom (f " ) = the
carrier of
R^1
by FUNCT_2:def 1;
A9:
rng f = [#] R^1
by A3, TOPS_2:def 5;
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:24;
A12:
<*a*> = |[a]|
;
then reconsider w =
<*a*> as
Element of
REAL 1
by EUCLID:25;
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:54;
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, EUCLID:69
.=
<*((1 - b) * a)*>
by RVSUM_1:69
;
thus (f * (G * [:(f " ),(id I[01] ):])) . x =
f . ((G * [:(f " ),(id I[01] ):]) . x)
by FUNCT_2:21
.=
f . (G . ([:(f " ),(id I[01] ):] . a,b))
by A7, FUNCT_2:21
.=
f . (G . ((f " ) . a),((id I[01] ) . b))
by A8, Lm4, FUNCT_3:def 9
.=
f . (G . ((f " ) . a),b)
by FUNCT_1:35
.=
f . ((1 - b) * ((f " ) . a))
by A1
.=
((1 - b) * ((f " ) . a)) /. 1
by A2
.=
<*z*> /. 1
by A11
.=
(1 - b) * a
by A15, FINSEQ_4:25
.=
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
by BORSUK_2:12;
G is continuous
by A1, TOPALG_1:18;
hence
F is continuous
by A4, A16, A6, FUNCT_2:113; verum