set E = the carrier of R^1;
let T be non empty interval SubSpace of R^1 ; :: thesis: for P, Q being continuous Function of I[01],T holds R1Homotopy (P,Q) is continuous
let P, Q be continuous Function of I[01],T; :: thesis: R1Homotopy (P,Q) is continuous
set F = R1Homotopy (P,Q);
set PI = [:P,(id I[01]):];
set QI = [:Q,(id I[01]):];
defpred S₁[ Element of the carrier of R^1, Element of the carrier of I[01], set ] means $3 = (1 - $2) * $1;
defpred S₂[ Element of the carrier of R^1, Element of the carrier of I[01], set ] means $3 = $2 * $1;
A1: the carrier of T is Subset of R^1 by TSEP_1:1;
then reconsider G = R1Homotopy (P,Q) as Function of [:I[01],I[01]:],R^1 by FUNCT_2:7;
reconsider P1 = P, Q1 = Q as Function of I[01],R^1 by A1, FUNCT_2:7;
reconsider P1 = P1, Q1 = Q1 as continuous Function of I[01],R^1 by PRE_TOPC:26;
set P1I = [:P1,(id I[01]):];
set Q1I = [:Q1,(id I[01]):];
A2: for x being Element of the carrier of R^1
for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S₁[x,y,z]

proof

let x be Element of the carrier of R^1; :: thesis: for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S₁[x,y,z]
let y be Element of the carrier of I[01]; :: thesis: ex z being Element of the carrier of R^1 st S₁[x,y,z]
(1 - y) * x in REAL by XREAL_0:def 1;
then reconsider z = (1 - y) * x as Element of the carrier of R^1 by TOPMETR:17;
take z ; :: thesis: S₁[x,y,z]
thus S₁[x,y,z] ; :: thesis: verum

end;

consider Pa being Function of [: the carrier of R^1, the carrier of I[01]:], the carrier of R^1 such that
A3: for x being Element of the carrier of R^1
for i being Element of the carrier of I[01] holds S₁[x,i,Pa . (x,i)] from BINOP_1:sch 3(A2);
A4: for x being Element of the carrier of R^1
for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S₂[x,y,z]

proof

let x be Element of the carrier of R^1; :: thesis: for y being Element of the carrier of I[01] ex z being Element of the carrier of R^1 st S₂[x,y,z]
let y be Element of the carrier of I[01]; :: thesis: ex z being Element of the carrier of R^1 st S₂[x,y,z]
y * x in REAL by XREAL_0:def 1;
hence ex z being Element of the carrier of R^1 st S₂[x,y,z] by TOPMETR:17; :: thesis: verum

end;

consider Pb being Function of [: the carrier of R^1, the carrier of I[01]:], the carrier of R^1 such that
A5: for x being Element of the carrier of R^1
for i being Element of the carrier of I[01] holds S₂[x,i,Pb . (x,i)] from BINOP_1:sch 3(A4);
reconsider Pa = Pa, Pb = Pb as Function of [:R^1,I[01]:],R^1 by Lm3;
A6: Pb is continuous by A5, Th7;
Pa is continuous by A3, Th6;
then consider g being Function of [:I[01],I[01]:],R^1 such that
A7: for p being Point of [:I[01],I[01]:]
for r1, r2 being Real st (Pa * [:P1,(id I[01]):]) . p = r1 & (Pb * [:Q1,(id I[01]):]) . p = r2 holds
g . p = r1 + r2 and
A8: g is continuous by A6, JGRAPH_2:19;
A9: 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

A10: dom Q = the carrier of I[01] by FUNCT_2:def 1;
A11: 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
A12: p = [s,t] by BORSUK_1:10;
reconsider a1 = P . s, b1 = Q . s as Point of R^1 by PRE_TOPC:25;
A13: P . s in the carrier of T ;
A14: (R1Homotopy (P,Q)) . (s,t) = ((1 - t) * a1) + (t * b1) by Def4;
A15: Q . s in the carrier of T ;
A16: (id I[01]) . t = t by FUNCT_1:18;
A17: (Pb * [:Q,(id I[01]):]) . p = Pb . ([:Q,(id I[01]):] . (s,t)) by A12, FUNCT_2:15
.= Pb . ((Q . s),t) by A10, A16, Lm4, FUNCT_3:def 8
.= t * (Q . s) by A1, A5, A15 ;
(Pa * [:P,(id I[01]):]) . p = Pa . ([:P,(id I[01]):] . (s,t)) by A12, FUNCT_2:15
.= Pa . ((P . s),t) by A11, A16, Lm4, FUNCT_3:def 8
.= (1 - t) * (P . s) by A1, A3, A13 ;
hence G . p = ((Pa * [:P1,(id I[01]):]) . p) + ((Pb * [:Q1,(id I[01]):]) . p) by A12, A17, A14; :: 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 A9
.= g . p by A7 ; :: thesis: verum

end;

hence R1Homotopy (P,Q) is continuous by A8, FUNCT_2:63, PRE_TOPC:27; :: thesis: verum