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.]

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

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 object ; :: according to TARSKI:def 3 :: thesis: ( not u in [.b,(a + b).] or u in (AffineMap (a,b)) .: [.0,1.] )
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 (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

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