let n be Nat; for P, Q being continuous Function of I[01] ,(TOP-REAL n) holds RealHomotopy P,Q is continuous
set I = the carrier of I[01] ;
let P, Q be continuous Function of I[01] ,(TOP-REAL n); RealHomotopy P,Q is continuous
set F = RealHomotopy P,Q;
set T = the carrier of (TOP-REAL n);
set PI = [:P,(id I[01] ):];
set QI = [:Q,(id I[01] ):];
A1:
( [:P,(id I[01] ):] is continuous & [:Q,(id I[01] ):] is continuous )
by BORSUK_2:12;
deffunc H1( Element of (TOP-REAL n), Element of the carrier of I[01] ) -> Element of the carrier of (TOP-REAL n) = $2 * $1;
deffunc H2( Element of (TOP-REAL n), Element of the carrier of I[01] ) -> Element of the carrier of (TOP-REAL n) = (1 - $2) * $1;
consider Pa being Function of [:the carrier of (TOP-REAL n),the carrier of I[01] :],the carrier of (TOP-REAL n) such that
A2:
for x being Element of the carrier of (TOP-REAL n)
for i being Element of the carrier of I[01] holds Pa . x,i = H2(x,i)
from BINOP_1:sch 4();
consider Pb being Function of [:the carrier of (TOP-REAL n),the carrier of I[01] :],the carrier of (TOP-REAL n) such that
A3:
for x being Element of the carrier of (TOP-REAL n)
for i being Element of the carrier of I[01] holds Pb . x,i = H1(x,i)
from BINOP_1:sch 4();
the carrier of [:(TOP-REAL n),I[01] :] = [:the carrier of (TOP-REAL n),the carrier of I[01] :]
by BORSUK_1:def 5;
then reconsider Pa = Pa, Pb = Pb as Function of [:(TOP-REAL n),I[01] :],(TOP-REAL n) ;
A4:
Pb is continuous
by A3, Th19;
A5:
for p being Point of [:I[01] ,I[01] :] holds (RealHomotopy P,Q) . p = ((Pa * [:P,(id I[01] ):]) . p) + ((Pb * [:Q,(id I[01] ):]) . p)
proof
A6:
dom Q = the
carrier of
I[01]
by FUNCT_2:def 1;
A7:
dom P = the
carrier of
I[01]
by FUNCT_2:def 1;
let p be
Point of
[:I[01] ,I[01] :];
(RealHomotopy P,Q) . p = ((Pa * [:P,(id I[01] ):]) . p) + ((Pb * [:Q,(id I[01] ):]) . p)
consider s,
t being
Point of
I[01] such that A8:
p = [s,t]
by BORSUK_1:50;
A9:
(
dom (id I[01] ) = the
carrier of
I[01] &
(id I[01] ) . t = t )
by FUNCT_1:35, FUNCT_2:def 1;
A10:
(Pb * [:Q,(id I[01] ):]) . p =
Pb . ([:Q,(id I[01] ):] . s,t)
by A8, FUNCT_2:21
.=
Pb . (Q . s),
t
by A6, A9, FUNCT_3:def 9
.=
t * (Q . s)
by A3
;
A11:
(Pa * [:P,(id I[01] ):]) . p =
Pa . ([:P,(id I[01] ):] . s,t)
by A8, FUNCT_2:21
.=
Pa . (P . s),
t
by A7, A9, FUNCT_3:def 9
.=
(1 - t) * (P . s)
by A2
;
thus (RealHomotopy P,Q) . p =
(RealHomotopy P,Q) . s,
t
by A8
.=
((Pa * [:P,(id I[01] ):]) . p) + ((Pb * [:Q,(id I[01] ):]) . p)
by A11, A10, Def7
;
verum
end;
Pa is continuous
by A2, Th18;
hence
RealHomotopy P,Q is continuous
by A1, A4, A5, Lm1; verum