let f be Function of R^1,R^1; :: thesis: for a, b being Real st a <> 0 & f = AffineMap (a,b) holds
f is being_homeomorphism
let a, b be Real; :: thesis: ( a <> 0 & f = AffineMap (a,b) implies f is being_homeomorphism )
assume that
A1: a <> 0 and
A2: f = AffineMap (a,b) ; :: thesis: f is being_homeomorphism
thus dom f = [#] R^1 by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng f = [#] R^1 & f is one-to-one & f is continuous & f " is continuous )
thus A3: rng f = [#] R^1 by A1, A2, FCONT_1:55, TOPMETR:17; :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus A4: f is one-to-one by A1, A2, FCONT_1:50; :: thesis: ( f is continuous & f " is continuous )
for x being Real holds f . x = (a * x) + b by A2, FCONT_1:def 4;
hence f is continuous by TOPMETR:21; :: thesis: f " is continuous
f is onto by A3, FUNCT_2:def 3;
then f " = f " by A4, TOPS_2:def 4
.= AffineMap ((a "),(- (b / a))) by A1, A2, FCONT_1:56 ;
then for x being Real holds (f ") . x = ((a ") * x) + (- (b / a)) by FCONT_1:def 4;
hence f " is continuous by TOPMETR:21; :: thesis: verum