let b, c be Real; :: thesis: ( c - b > 0 implies rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) = [.0,1.] )
set f = AffineMap ((- (1 / (c - b))),(c / (c - b)));
set g = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.];
assume A0: c - b > 0 ; :: thesis: rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) = [.0,1.]
thus rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) c= [.0,1.] :: according to XBOOLE_0:def 10 :: thesis: [.0,1.] c= rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) or y in [.0,1.] )
assume Y0: y in rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) ; :: thesis: y in [.0,1.]
then consider x being object such that
A1: x in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) and
A2: y = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x by FUNCT_1:def 3;
Y1: x in [.b,c.] by A1, RELAT_1:57;
reconsider xx = x as Real by A1;
reconsider yy = y as Real by Y0;
S4: y = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . xx by FUNCT_1:47, A1, A2;
A4: b <= xx by Y1, XXREAL_1:1;
S2: (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b = 1 by Cb1, A0;
S5: (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b >= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . xx by A4, FCONT_1:54, A0;
xx <= c by Y1, XXREAL_1:1;
then S6: (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . xx >= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . c by A0, FCONT_1:54;
(AffineMap ((- (1 / (c - b))),(c / (c - b)))) . c = 0 by Cb2;
hence y in [.0,1.] by S4, S2, S5, S6; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [.0,1.] or y in rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) )
assume V1: y in [.0,1.] ; :: thesis: y in rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])
then reconsider yy = y as Real ;
set A = - (1 / (c - b));
set B = c / (c - b);
L2: (AffineMap ((- (1 / (c - b))),(c / (c - b)))) " = AffineMap (((- (1 / (c - b))) "),(- ((c / (c - b)) / (- (1 / (c - b)))))) by FCONT_1:56, A0;
then L3: ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . 0 = (((- (1 / (c - b))) ") * 0) + (- ((c / (c - b)) / (- (1 / (c - b))))) by FCONT_1:def 4
.= - ((c / (c - b)) / ((- 1) / (c - b))) by XCMPLX_1:187
.= - (c / (- 1)) by XCMPLX_1:55, A0
.= c ;
X1: - ((c / (c - b)) / (- (1 / (c - b)))) = - ((c / (c - b)) / ((- 1) / (c - b))) by XCMPLX_1:187
.= - (c / (- 1)) by XCMPLX_1:55, A0
.= c ;
L4: ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . 1 = (((- (1 / (c - b))) ") * 1) + (- ((c / (c - b)) / (- (1 / (c - b))))) by FCONT_1:def 4, L2
.= (1 / (- (1 / (c - b)))) + (- ((c / (c - b)) / (- (1 / (c - b))))) by XCMPLX_1:215
.= (1 / ((- 1) / (c - b))) + c by XCMPLX_1:187, X1
.= ((c - b) / (- 1)) + c by XCMPLX_1:57
.= b ;
set x = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy;
reconsider xx = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy as Real by L2;
J2: ( 0 <= yy & yy <= 1 ) by XXREAL_1:1, V1;
then J3: c >= xx by FCONT_1:54, L2, A0, L3;
xx >= b by FCONT_1:54, L2, A0, J2, L4;
then J4: ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy in [.b,c.] by J3;
jj: dom (AffineMap ((- (1 / (c - b))),(c / (c - b)))) = REAL by FUNCT_2:def 1;
T1: ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by J4, jj, RELAT_1:57;
rng (AffineMap ((- (1 / (c - b))),(c / (c - b)))) = REAL by FCONT_1:55, A0;
then S2: yy in rng (AffineMap ((- (1 / (c - b))),(c / (c - b)))) by XREAL_0:def 1;
set ff = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) " ;
((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . (((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy) = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . (((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy) by FUNCT_1:49, J4
.= yy by A0, S2, FUNCT_1:35 ;
hence y in rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) by T1, FUNCT_1:def 3; :: thesis: verum