let n be Element of NAT ; :: thesis: for T being non empty convex SubSpace of TOP-REAL n
for P, Q being continuous Function of I[01] ,T holds ConvexHomotopy P,Q is continuous
let T be non empty convex SubSpace of TOP-REAL n; :: thesis: for P, Q being continuous Function of I[01] ,T holds ConvexHomotopy P,Q is continuous
let P, Q be continuous Function of I[01] ,T; :: thesis: ConvexHomotopy P,Q is continuous
set F = ConvexHomotopy P,Q;
A1: the carrier of T is Subset of (TOP-REAL n) by TSEP_1:1;
then reconsider G = ConvexHomotopy P,Q as Function of [:I[01] ,I[01] :],(TOP-REAL n) by FUNCT_2:9;
reconsider P1 = P, Q1 = Q as Function of I[01] ,(TOP-REAL n) by A1, FUNCT_2:9;
set E = the carrier of (TOP-REAL n);
set PI = [:P,(id I[01] ):];
set QI = [:Q,(id I[01] ):];
reconsider P1 = P1, Q1 = Q1 as continuous Function of I[01] ,(TOP-REAL n) by PRE_TOPC:56;
set P1I = [:P1,(id I[01] ):];
set Q1I = [:Q1,(id I[01] ):];
A2: ( [:P1,(id I[01] ):] is continuous & [:Q1,(id I[01] ):] is continuous ) by BORSUK_2:12;
deffunc H₁( Element of the carrier of (TOP-REAL n), Element of the carrier of I[01] ) -> Element of the carrier of (TOP-REAL n) = $2 * $1;
deffunc H₂( Element of the carrier 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
A3: 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 = H₂(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
A4: 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 = H₁(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) ;
A5: Pb is continuous by A4, TOPALG_1:19;
Pa is continuous by A3, TOPALG_1:18;
then consider g being Function of [:I[01] ,I[01] :],(TOP-REAL n) such that
A6: for r being Point of [:I[01] ,I[01] :] holds g . r = ((Pa * [:P1,(id I[01] ):]) . r) + ((Pb * [:Q1,(id I[01] ):]) . r) and
A7: g is continuous by A2, A5, JGRAPH_6:20;
A8: for p being Point of [:I[01] ,I[01] :] holds G . p = ((Pa * [:P1,(id I[01] ):]) . p) + ((Pb * [:Q1,(id I[01] ):]) . p)

proof

A9: dom Q = the carrier of I[01] by FUNCT_2:def 1;
A10: dom P = the carrier of I[01] by FUNCT_2:def 1;
let p be Point of [:I[01] ,I[01] :]; :: thesis: G . p = ((Pa * [:P1,(id I[01] ):]) . p) + ((Pb * [:Q1,(id I[01] ):]) . p)
consider s, t being Point of I[01] such that
A11: p = [s,t] by BORSUK_1:50;
reconsider a1 = P . s, b1 = Q . s as Point of (TOP-REAL n) by PRE_TOPC:55;
A12: (ConvexHomotopy P,Q) . s,t = ((1 - t) * a1) + (t * b1) by Def2;
A13: (id I[01] ) . t = t by FUNCT_1:35;
A14: (Pb * [:Q,(id I[01] ):]) . p = Pb . ([:Q,(id I[01] ):] . s,t) by A11, FUNCT_2:21
.= Pb . (Q . s),t by A9, A13, Lm4, FUNCT_3:def 9
.= t * (Q1 . s) by A4 ;
(Pa * [:P,(id I[01] ):]) . p = Pa . ([:P,(id I[01] ):] . s,t) by A11, FUNCT_2:21
.= Pa . (P . s),t by A10, A13, Lm4, FUNCT_3:def 9
.= (1 - t) * (P1 . s) by A3 ;
hence G . p = ((Pa * [:P1,(id I[01] ):]) . p) + ((Pb * [:Q1,(id I[01] ):]) . p) by A11, A14, A12; :: thesis: verum

end;

for p being Point of [:I[01] ,I[01] :] holds G . p = g . p

proof

let p be Point of [:I[01] ,I[01] :]; :: thesis: G . p = g . p
thus G . p = ((Pa * [:P1,(id I[01] ):]) . p) + ((Pb * [:Q1,(id I[01] ):]) . p) by A8
.= g . p by A6 ; :: thesis: verum

end;

hence ConvexHomotopy P,Q is continuous by A7, FUNCT_2:113, PRE_TOPC:57; :: thesis: verum