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, Th32, TOPMETR:24; :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus A4: f is one-to-one by A1, A2, Th27; :: thesis: ( f is continuous & f " is continuous )
for x being Real holds f . x = (a * x) + b by A2, Def3;
hence f is continuous by TOPMETR:28; :: thesis: f " is continuous
f " = f " by A3, A4, TOPS_2:def 4
.= AffineMap (a " ),(- (b / a)) by A1, A2, Th33 ;
then for x being Real holds (f " ) . x = ((a " ) * x) + (- (b / a)) by Def3;
hence f " is continuous by TOPMETR:28; :: thesis: verum