thus rng (AffineMap (a,b)) = REAL by JORDAN16:32; :: according to FUNCT_2:def 3 :: thesis: AffineMap (a,b) is one-to-one
thus AffineMap (a,b) is one-to-one by JORDAN16:27; :: thesis: verum