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,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,T holds ConvexHomotopy (P,Q) is continuous
let P, Q be continuous Function of I,T; :: thesis: ConvexHomotopy (P,Q) is continuous
set F = ConvexHomotopy (P,Q);
A1: the carrier of T is Subset of () by TSEP_1:1;
then reconsider G = ConvexHomotopy (P,Q) as Function of ,() by FUNCT_2:7;
reconsider P1 = P, Q1 = Q as Function of I,() by ;
set E = the carrier of ();
set PI = [:P,():];
set QI = [:Q,():];
reconsider P1 = P1, Q1 = Q1 as continuous Function of I,() by PRE_TOPC:26;
set P1I = [:P1,():];
set Q1I = [:Q1,():];
deffunc H1( Element of the carrier of (), Element of the carrier of I) -> Element of the carrier of () = \$2 * \$1;
deffunc H2( Element of the carrier of (), Element of the carrier of I) -> Element of the carrier of () = (1 - \$2) * \$1;
consider Pa being Function of [: the carrier of (), the carrier of I:], the carrier of () such that
A2: for x being Element of the carrier of ()
for i being Element of the carrier of I holds Pa . (x,i) = H2(x,i) from consider Pb being Function of [: the carrier of (), the carrier of I:], the carrier of () such that
A3: for x being Element of the carrier of ()
for i being Element of the carrier of I holds Pb . (x,i) = H1(x,i) from the carrier of [:(),I:] = [: the carrier of (), the carrier of I:] by BORSUK_1:def 2;
then reconsider Pa = Pa, Pb = Pb as Function of [:(),I:],() ;
A4: Pb is continuous by ;
Pa is continuous by ;
then consider g being Function of ,() such that
A5: for r being Point of holds g . r = ((Pa * [:P1,():]) . r) + ((Pb * [:Q1,():]) . r) and
A6: g is continuous by ;
A7: for p being Point of holds G . p = ((Pa * [:P1,():]) . p) + ((Pb * [:Q1,():]) . p)
proof
A8: dom Q = the carrier of I by FUNCT_2:def 1;
A9: dom P = the carrier of I by FUNCT_2:def 1;
let p be Point of ; :: thesis: G . p = ((Pa * [:P1,():]) . p) + ((Pb * [:Q1,():]) . p)
consider s, t being Point of I such that
A10: p = [s,t] by BORSUK_1:10;
reconsider a1 = P . s, b1 = Q . s as Point of () by PRE_TOPC:25;
A11: (ConvexHomotopy (P,Q)) . (s,t) = ((1 - t) * a1) + (t * b1) by Def2;
A12: (id I) . t = t by FUNCT_1:18;
A13: (Pb * [:Q,():]) . p = Pb . ([:Q,():] . (s,t)) by
.= Pb . ((Q . s),t) by
.= t * (Q1 . s) by A3 ;
(Pa * [:P,():]) . p = Pa . ([:P,():] . (s,t)) by
.= Pa . ((P . s),t) by
.= (1 - t) * (P1 . s) by A2 ;
hence G . p = ((Pa * [:P1,():]) . p) + ((Pb * [:Q1,():]) . p) by ; :: thesis: verum
end;
for p being Point of holds G . p = g . p
proof
let p be Point of ; :: thesis: G . p = g . p
thus G . p = ((Pa * [:P1,():]) . p) + ((Pb * [:Q1,():]) . p) by A7
.= g . p by A5 ; :: thesis: verum
end;
hence ConvexHomotopy (P,Q) is continuous by ; :: thesis: verum