let a, b be Real; :: 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

A2: (AffineMap (a,b)) . 1 = a + b by Th49;
let u be object ; :: 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
A3: r in [.0,1.] and
A4: u = (AffineMap (a,b)) . r by FUNCT_2:65;
reconsider s = u as Real by A4;
r <= 1 by A3, XXREAL_1:1;
then A5: s <= a + b by A1, A4, A2, Th53;
A6: (AffineMap (a,b)) . 0 = b by Th48;
0 <= r by A3, XXREAL_1:1;
then b <= s by A1, A4, A6, Th53;
hence u in [.b,(a + b).] by A5, XXREAL_1:1; :: thesis: verum

end;

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in [.b,(a + b).] or u in (AffineMap (a,b)) .: [.0,1.] )
assume A7: 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;
A8: (AffineMap (a,b)) . ((r - b) / a) = (a * ((r - b) / a)) + b by Def4
.= (r - b) + b by A1, XCMPLX_1:87
.= r ;
r <= a + b by A7, XXREAL_1:1;
then r - b <= a by XREAL_1:20;
then (r - b) / a <= a / a by A1, XREAL_1:72;
then A9: (r - b) / a <= 1 by A1, XCMPLX_1:60;
b <= r by A7, XXREAL_1:1;
then 0 <= r - b by XREAL_1:48;
then (r - b) / a in [.0,1.] by A1, A9, XXREAL_1:1;
hence u in (AffineMap (a,b)) .: [.0,1.] by A8, FUNCT_2:35; :: thesis: verum