let a, b be real number ; :: thesis: ( a > 0 implies (AffineMap a,b) .: [.0 ,1.] = [.b,(a + b).] )
assume A1: a > 0 ; :: thesis: (AffineMap a,b) .: [.0 ,1.] = [.b,(a + b).]
thus (AffineMap a,b) .: [.0 ,1.] c= [.b,(a + b).] :: according to XBOOLE_0:def 10 :: thesis: [.b,(a + b).] c= (AffineMap a,b) .: [.0 ,1.]

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in (AffineMap a,b) .: [.0 ,1.] or u in [.b,(a + b).] )
assume u in (AffineMap a,b) .: [.0 ,1.] ; :: thesis: u in [.b,(a + b).]
then consider r being Element of REAL such that
A2: r in [.0 ,1.] and
A3: u = (AffineMap a,b) . r by FUNCT_2:116;
reconsider s = u as real number by A3;
A4: (AffineMap a,b) . 0 = b by Th25;
A5: (AffineMap a,b) . 1 = a + b by Th26;
( 0 <= r & r <= 1 ) by A2, XXREAL_1:1;
then ( b <= s & s <= a + b ) by A1, A3, A4, A5, Th30;
hence u in [.b,(a + b).] by XXREAL_1:1; :: thesis: verum

end;

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in [.b,(a + b).] or u in (AffineMap a,b) .: [.0 ,1.] )
assume A6: u in [.b,(a + b).] ; :: thesis: u in (AffineMap a,b) .: [.0 ,1.]
then reconsider r = u as Element of REAL ;
set s = (r - b) / a;
b <= r by A6, XXREAL_1:1;
then 0 <= r - b by XREAL_1:50;
then A7: 0 <= (r - b) / a by A1;
r <= a + b by A6, XXREAL_1:1;
then r - b <= a by XREAL_1:22;
then (r - b) / a <= a / a by A1, XREAL_1:74;
then (r - b) / a <= 1 by A1, XCMPLX_1:60;
then A8: (r - b) / a in [.0 ,1.] by A7, XXREAL_1:1;
(AffineMap a,b) . ((r - b) / a) = (a * ((r - b) / a)) + b by Def3
.= (r - b) + b by A1, XCMPLX_1:88
.= r ;
hence u in (AffineMap a,b) .: [.0 ,1.] by A8, FUNCT_2:43; :: thesis: verum