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]):];
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
A1:
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
A2:
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 2;
then reconsider Pa = Pa, Pb = Pb as Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) ;
A3:
Pb is continuous
by A2, Th18;
A4:
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
A5:
dom Q = the
carrier of
I[01]
by FUNCT_2:def 1;
A6:
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 A7:
p = [s,t]
by BORSUK_1:10;
A8:
(
dom (id I[01]) = the
carrier of
I[01] &
(id I[01]) . t = t )
by FUNCT_1:18, FUNCT_2:def 1;
A9:
(Pb * [:Q,(id I[01]):]) . p =
Pb . ([:Q,(id I[01]):] . (s,t))
by A7, FUNCT_2:15
.=
Pb . (
(Q . s),
t)
by A5, A8, FUNCT_3:def 8
.=
t * (Q . s)
by A2
;
A10:
(Pa * [:P,(id I[01]):]) . p =
Pa . ([:P,(id I[01]):] . (s,t))
by A7, FUNCT_2:15
.=
Pa . (
(P . s),
t)
by A6, A8, FUNCT_3:def 8
.=
(1 - t) * (P . s)
by A1
;
thus (RealHomotopy (P,Q)) . p =
(RealHomotopy (P,Q)) . (
s,
t)
by A7
.=
((Pa * [:P,(id I[01]):]) . p) + ((Pb * [:Q,(id I[01]):]) . p)
by A10, A9, Def7
;
verum
end;
Pa is continuous
by A1, Th17;
hence
RealHomotopy (P,Q) is continuous
by A3, A4, Lm1; verum