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