let a, b be Real; :: thesis: ( b - a > 0 implies rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) = [.0,1.] )
set f = AffineMap ((1 / (b - a)),(- (a / (b - a))));
set g = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.];
assume A0: b - a > 0 ; :: thesis: rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) = [.0,1.]
thus rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) c= [.0,1.] :: according to XBOOLE_0:def 10 :: thesis: [.0,1.] c= rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) or y in [.0,1.] )
assume Y0: y in rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) ; :: thesis: y in [.0,1.]
then consider x being object such that
A1: x in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) and
A2: y = ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . x by FUNCT_1:def 3;
Y1: x in [.a,b.] by A1, RELAT_1:57;
reconsider xx = x as Real by A1;
reconsider yy = y as Real by Y0;
S4: y = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . xx by FUNCT_1:47, A1, A2;
A4: a <= xx by Y1, XXREAL_1:1;
S2: (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . a = 0 by Ah1;
S5: (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . a <= (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . xx by A4, FCONT_1:53, A0;
xx <= b by Y1, XXREAL_1:1;
then S6: (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . xx <= (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . b by A0, FCONT_1:53;
(AffineMap ((1 / (b - a)),(- (a / (b - a))))) . b = 1 by Ab1, A0;
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 / (b - a)),(- (a / (b - a))))) | [.a,b.]) )
assume V1: y in [.0,1.] ; :: thesis: y in rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])
then reconsider yy = y as Real ;
set A = 1 / (b - a);
set B = - (a / (b - a));
L2: (AffineMap ((1 / (b - a)),(- (a / (b - a))))) " = AffineMap (((1 / (b - a)) "),(- ((- (a / (b - a))) / (1 / (b - a))))) by A0, FCONT_1:56;
then L3: ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) ") . 0 = (((1 / (b - a)) ") * 0) + (- ((- (a / (b - a))) / (1 / (b - a)))) by FCONT_1:def 4
.= - (((- a) / (b - a)) / (1 / (b - a))) by XCMPLX_1:187
.= - ((- a) / 1) by XCMPLX_1:55, A0
.= a ;
set x = ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) ") . yy;
reconsider xx = ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) ") . yy as Real by L2;
X1: - ((- (a / (b - a))) / (1 / (b - a))) = - (((- a) / (b - a)) / (1 / (b - a))) by XCMPLX_1:187
.= - ((- a) / 1) by XCMPLX_1:55, A0
.= a ;
L4: ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) ") . 1 = (((1 / (b - a)) ") * 1) + (- ((- (a / (b - a))) / (1 / (b - a)))) by FCONT_1:def 4, L2
.= (1 / (1 / (b - a))) + (- ((- (a / (b - a))) / (1 / (b - a)))) by XCMPLX_1:215
.= (b - a) + a by XCMPLX_1:52, X1
.= b ;
J2: ( 0 <= yy & yy <= 1 ) by XXREAL_1:1, V1;
then J3: a <= xx by FCONT_1:53, L2, A0, L3;
xx <= b by FCONT_1:53, L2, A0, J2, L4;
then J4: ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) ") . yy in [.a,b.] by J3;
j5: dom (AffineMap ((1 / (b - a)),(- (a / (b - a))))) = REAL by FUNCT_2:def 1;
T1: ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) ") . yy in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by J4, j5, RELAT_1:57;
rng (AffineMap ((1 / (b - a)),(- (a / (b - a))))) = REAL by FCONT_1:55, A0;
then S2: yy in rng (AffineMap ((1 / (b - a)),(- (a / (b - a))))) by XREAL_0:def 1;
((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) ") . yy) = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) ") . yy) by FUNCT_1:49, J4
.= yy by A0, S2, FUNCT_1:35 ;
hence y in rng ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) by T1, FUNCT_1:def 3; :: thesis: verum