A1: ( 0 = (#) (0,1) & 1 = (0,1) (#) ) by TREAL_1:def 1, TREAL_1:def 2;
let a, b, c, d be Real; :: thesis: ( a < b & c <= d implies for x being Real st a <= x & x <= b holds
(L[01] (a,b,c,d)) . x = (((d - c) / (b - a)) * (x - a)) + c )
assume A2: a < b ; :: thesis: ( not c <= d or for x being Real st a <= x & x <= b holds
(L[01] (a,b,c,d)) . x = (((d - c) / (b - a)) * (x - a)) + c )
set G = P[01] (a,b,((#) (0,1)),((0,1) (#)));
set F = L[01] (((#) (c,d)),((c,d) (#)));
set f = L[01] (a,b,c,d);
assume A3: c <= d ; :: thesis: for x being Real st a <= x & x <= b holds
(L[01] (a,b,c,d)) . x = (((d - c) / (b - a)) * (x - a)) + c
then A4: ( (#) (c,d) = c & (c,d) (#) = d ) by TREAL_1:def 1, TREAL_1:def 2;
let x be Real; :: thesis: ( a <= x & x <= b implies (L[01] (a,b,c,d)) . x = (((d - c) / (b - a)) * (x - a)) + c )
assume A5: a <= x ; :: thesis: ( not x <= b or (L[01] (a,b,c,d)) . x = (((d - c) / (b - a)) * (x - a)) + c )
set X = (x - a) / (b - a);
assume A6: x <= b ; :: thesis: (L[01] (a,b,c,d)) . x = (((d - c) / (b - a)) * (x - a)) + c
then A7: (x - a) / (b - a) in the carrier of (Closed-Interval-TSpace (0,1)) by A5, Th2;
x in [.a,b.] by A5, A6, XXREAL_1:1;
then A8: x in the carrier of (Closed-Interval-TSpace (a,b)) by A2, TOPMETR:18;
then x in dom (P[01] (a,b,((#) (0,1)),((0,1) (#)))) by FUNCT_2:def 1;
then (L[01] (a,b,c,d)) . x = (L[01] (((#) (c,d)),((c,d) (#)))) . ((P[01] (a,b,((#) (0,1)),((0,1) (#)))) . x) by FUNCT_1:13
.= (L[01] (((#) (c,d)),((c,d) (#)))) . ((((b - x) * 0) + ((x - a) * 1)) / (b - a)) by A2, A8, A1, TREAL_1:def 4
.= ((1 - ((x - a) / (b - a))) * c) + (((x - a) / (b - a)) * d) by A3, A4, A7, TREAL_1:def 3
.= (((d - c) / (b - a)) * (x - a)) + c by XCMPLX_1:234 ;
hence (L[01] (a,b,c,d)) . x = (((d - c) / (b - a)) * (x - a)) + c ; :: thesis: verum