let A be Subset of (TOP-REAL 2); :: thesis:
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis:
assume that
A1: A is_an_arc_of p1,p2 and
A2: ( LE q1,q2,A,p1,p2 & q1 <> q2 ) ; :: thesis:
consider g being Function of I[01],((TOP-REAL 2) | A), s1, s2 being Real such that
A3: g is being_homeomorphism and
A4: ( g . 0 = p1 & g . 1 = p2 ) and
A5: g . s1 = q1 and
A6: g . s2 = q2 and
A7: 0 <= s1 and
A8: s1 < s2 and
A9: s2 <= 1 by A1, A2, Th17;
reconsider A9 = A as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;
set S = Segment (A,p1,p2,q1,q2);
A10: Segment (A,p1,p2,q1,q2) = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,A,p1,p2 & LE q,q2,A,p1,p2 ) } by JORDAN6:26;
A11: 0 < s2 - s1 by A8, XREAL_1:50;
set f = (g * (AffineMap ((s2 - s1),s1))) | [.0,1.];
reconsider g = g as Function of I[01],((TOP-REAL 2) | A9) ;
reconsider m = AffineMap ((s2 - s1),s1) as Function of R^1,R^1 by TOPMETR:17;
for x being Real holds m . x = ((s2 - s1) * x) + s1 by FCONT_1:def 4;
then reconsider m = m as continuous Function of R^1,R^1 by TOPMETR:21;
set h = m | I[01];
A12: m | I[01] = m | [.0,1.] by BORSUK_1:40, TMAP_1:def 4;
then A13: rng (m | I[01]) = m .: [.0,1.] by RELAT_1:115
.= [.s1,((s2 - s1) + s1).] by A8, FCONT_1:57, XREAL_1:50
.= [.s1,s2.] ;
then A14: rng (m | I[01]) c= [.0,1.] by A7, A9, XXREAL_1:34;
A15: dom m = REAL by FUNCT_2:def 1;
then A16: dom (m | I[01]) = [.0,1.] by A12, RELAT_1:62;
then reconsider h = m | I[01] as Function of I[01],I[01] by A14, BORSUK_1:40, RELSET_1:4;
A17: (g * (AffineMap ((s2 - s1),s1))) | [.0,1.] = g * h by A12, RELAT_1:83;
A18: [.0,1.] = dom g by BORSUK_1:40, FUNCT_2:def 1;
m .: [.0,1.] c= dom g

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in m .: [.0,1.] ; :: thesis:
then A19: e in [.s1,((s2 - s1) + s1).] by A8, FCONT_1:57, XREAL_1:50;
[.s1,s2.] c= [.0,1.] by A7, A9, XXREAL_1:34;
hence e in dom g by A18, A19; :: thesis:

end;

then A20: [.0,1.] c= dom (g * m) by A15, FUNCT_3:3;
then A21: dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) = [#] I[01] by BORSUK_1:40, RELAT_1:62;
reconsider CIT = Closed-Interval-TSpace (s1,s2) as non empty SubSpace of I[01] by A7, A8, A9, TOPMETR:20, TREAL_1:3;
[.s1,s2.] c= [.0,1.] by A7, A9, XXREAL_1:34;
then A22: the carrier of CIT c= dom g by A8, A18, TOPMETR:18;
A23: rng h = the carrier of CIT by A8, A13, TOPMETR:18;
A24: dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) = the carrier of I[01] by A20, BORSUK_1:40, RELAT_1:62;
A25: s1 < 1 by A8, A9, XXREAL_0:2;
for y being object holds
( y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) iff ex x being object st
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ) )

proof

let y be object ; :: thesis:
thus ( y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) implies ex x being object st
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ) ) :: thesis:

proof

assume y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) ; :: thesis:
then y in Segment (A,p1,p2,q1,q2) by PRE_TOPC:def 5;
then consider q0 being Point of (TOP-REAL 2) such that
A26: y = q0 and
A27: LE q1,q0,A,p1,p2 and
A28: LE q0,q2,A,p1,p2 by A10;
q0 in A by A27, JORDAN5C:def 3;
then q0 in [#] ((TOP-REAL 2) | A) by PRE_TOPC:def 5;
then q0 in rng g by A3;
then consider s being object such that
A29: s in dom g and
A30: q0 = g . s by FUNCT_1:def 3;
reconsider s = s as Real by A29;
take x = (s - s1) / (s2 - s1); :: thesis:
A31: s <= 1 by A29, BORSUK_1:40, XXREAL_1:1;
then s <= s2 by A3, A4, A6, A7, A8, A9, A28, A30, JORDAN5C:def 3;
then s - s1 <= s2 - s1 by XREAL_1:9;
then x <= (s2 - s1) / (s2 - s1) by A11, XREAL_1:72;
then A32: x <= 1 by A11, XCMPLX_1:60;
0 <= s by A29, BORSUK_1:40, XXREAL_1:1;
then s1 + 0 <= s by A3, A4, A5, A25, A27, A30, A31, JORDAN5C:def 3;
then 0 <= s - s1 by XREAL_1:19;
hence A33: x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) by A11, A21, A32, BORSUK_1:40, XXREAL_1:1; :: thesis:
A34: x in REAL by XREAL_0:def 1;
m . x = ((s2 - s1) * x) + s1 by FCONT_1:def 4
.= (s - s1) + s1 by A11, XCMPLX_1:87
.= s ;
hence y = (g * m) . x by A15, A26, A30, FUNCT_1:13, A34
.= ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x by A33, FUNCT_1:47 ;
:: thesis:

end;

given x being object such that A35: x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) and
A36: y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ; :: thesis:
reconsider x = x as Element of REAL by A35;
(AffineMap ((s2 - s1),s1)) . x in REAL ;
then reconsider s = m . x as Element of REAL ;
h . x = m . x by A12, A16, A21, A35, BORSUK_1:40, FUNCT_1:47;
then A37: s in rng h by A16, A21, A35, BORSUK_1:40, FUNCT_1:def 3;
then A38: s1 <= s by A13, XXREAL_1:1;
y in rng ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) by A35, A36, FUNCT_1:def 3;
then y in [#] ((TOP-REAL 2) | A) ;
then y in A by PRE_TOPC:def 5;
then reconsider q = y as Point of (TOP-REAL 2) ;
A39: s <= s2 by A13, A37, XXREAL_1:1;
then A40: s <= 1 by A9, XXREAL_0:2;
A41: q = (g * m) . x by A35, A36, FUNCT_1:47
.= g . s by A15, FUNCT_1:13 ;
then A42: LE q1,q,A,p1,p2 by A1, A3, A4, A5, A7, A25, A38, A40, JORDAN5C:8;
LE q,q2,A,p1,p2 by A1, A3, A4, A6, A7, A9, A41, A38, A39, A40, JORDAN5C:8;
then q in Segment (A,p1,p2,q1,q2) by A10, A42;
hence y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) by PRE_TOPC:def 5; :: thesis:

end;

then A43: rng ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) = [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) by FUNCT_1:def 3;
then A44: [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) <> {} by A21, RELAT_1:42;
then reconsider f = (g * (AffineMap ((s2 - s1),s1))) | [.0,1.] as Function of I[01],((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) by A24, A43, FUNCT_2:def 1, RELSET_1:4;
reconsider TS = (TOP-REAL 2) | (Segment (A,p1,p2,q1,q2)) as non empty SubSpace of (TOP-REAL 2) | A9 by A44, Th2, TOPMETR:22;
take f ; :: according to TOPREAL1:def 1 :: thesis:
A45: (AffineMap ((s2 - s1),s1)) . 0 = s1 by FCONT_1:48;
set o = g | CIT;
A46: dom (g | CIT) = dom (g | the carrier of CIT) by TMAP_1:def 4
.= (dom g) /\ the carrier of CIT by RELAT_1:61
.= the carrier of CIT by A22, XBOOLE_1:28 ;
reconsider h = h as Function of I[01],CIT by A16, A23, RELSET_1:4;
h is onto by A23, FUNCT_2:def 3;
then A47: h is being_homeomorphism by A11, Th9, Th20;
A48: the carrier of CIT = [.s1,s2.] by A8, TOPMETR:18;
then g | CIT = g | (rng h) by A13, TMAP_1:def 4;
then A49: f = (g | CIT) * h by A17, FUNCT_4:2;
then A50: rng (g | CIT) = rng f by A13, A46, A48, RELAT_1:28;
then reconsider o = g | CIT as Function of CIT,TS by A46, RELSET_1:4;
o is onto by A43, A50, FUNCT_2:def 3;
then o is being_homeomorphism by A3, Th9;
hence f is being_homeomorphism by A49, A47, TOPS_2:57; :: thesis:
A51: dom (AffineMap ((s2 - s1),s1)) = REAL by FUNCT_2:def 1;
A52: 0 in REAL by XREAL_0:def 1;
0 in [.0,1.] by XXREAL_1:1;
hence f . 0 = (g * m) . 0 by FUNCT_1:49
.= q1 by A5, A45, A51, FUNCT_1:13, A52 ;
:: thesis:
A53: (AffineMap ((s2 - s1),s1)) . 1 = (s2 - s1) + s1 by FCONT_1:49
.= s2 ;
A54: 1 in REAL by XREAL_0:def 1;
1 in [.0,1.] by XXREAL_1:1;
hence f . 1 = (g * m) . 1 by FUNCT_1:49
.= q2 by A6, A53, A51, FUNCT_1:13, A54 ;
:: thesis: