let F be Function of [:R^1 ,I[01] :],R^1 ; :: thesis: ( ( 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 A1:
for x being Point of R^1
for i being Point of I[01] holds F . x,i = (1 - i) * x
; :: thesis: F is continuous
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
A2:
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;
A3:
G is continuous
by A2, TOPALG_1:18;
consider f being Function of (TOP-REAL 1),R^1 such that
A4:
for p being Element of (TOP-REAL 1) holds f . p = Proj p,1
by JORDAN2B:1;
A5:
f is being_homeomorphism
by A4, JORDAN2B:34;
then A6:
f is continuous
by TOPS_2:def 5;
f " is continuous
by A5, TOPS_2:def 5;
then
[:(f " ),(id I[01] ):] is continuous
by BORSUK_2:12;
then
G * [:(f " ),(id I[01] ):] is continuous
by A3;
then A7:
f * (G * [:(f " ),(id I[01] ):]) is continuous
by A6;
for x being Point of [:R^1 ,I[01] :] holds F . x = (f * (G * [:(f " ),(id I[01] ):])) . x
proof
let x be
Point of
[:R^1 ,I[01] :];
:: thesis: F . x = (f * (G * [:(f " ),(id I[01] ):])) . x
consider a being
Point of
R^1 ,
b being
Point of
I[01] such that A8:
x = [a,b]
by BORSUK_1:50;
A9:
dom f = the
carrier of
(TOP-REAL 1)
by FUNCT_2:def 1;
A10:
dom (f " ) = the
carrier of
R^1
by FUNCT_2:def 1;
reconsider ff =
f as
Function ;
set g =
ff " ;
A11:
rng f = [#] R^1
by A5, TOPS_2:def 5;
A12:
ff is
one-to-one
by A5, TOPS_2:def 5;
A13:
<*a*> = |[a]|
;
consider z being
Real such that A14:
(1 - b) * ((f " ) . a) = <*z*>
by JORDAN2B:24;
B14:
(1 - b) * ((f /" ) . a) = <*z*>
by A14, TOPS_2:def 4;
reconsider w =
<*a*> as
Element of
REAL 1
by A13, EUCLID:25;
f . <*a*> =
Proj |[a]|,1
by A4
.=
a
by Th4
;
then
<*a*> = (ff " ) . a
by A9, A12, A13, FUNCT_1:54;
then X:
w = (f /" ) . a
by A11, A12, TOPS_2:def 4;
A15:
<*z*> =
(1 - b) * ((f /" ) . a)
by A12, A14, TOPS_2:def 4, B14
.=
(1 - b) * w
by A14, TOPS_2:def 4, B14, X, 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 A8, FUNCT_2:21
.=
f . (G . ((f " ) . a),((id I[01] ) . b))
by A10, Lm4, FUNCT_3:def 9
.=
f . (G . ((f " ) . a),b)
by FUNCT_1:35
.=
f . ((1 - b) * ((f " ) . a))
by A2
.=
Proj ((1 - b) * ((f " ) . a)),1
by A4
.=
<*z*> /. 1
by A14, JORDAN2B:def 1
.=
(1 - b) * a
by A15, FINSEQ_4:25
.=
F . a,
b
by A1
.=
F . x
by A8
;
:: thesis: verum
end;
hence
F is continuous
by A7, FUNCT_2:113; :: thesis: verum