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