let a, b be real number ; :: thesis: ( a <> 0 implies AffineMap a,b is one-to-one )
assume A1: a <> 0 ; :: thesis: AffineMap a,b is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 (AffineMap a,b) or not x2 in proj1 (AffineMap a,b) or not (AffineMap a,b) . x1 = (AffineMap a,b) . x2 or x1 = x2 )
set f = AffineMap a,b;
assume x1 in dom (AffineMap a,b) ; :: thesis: ( not x2 in proj1 (AffineMap a,b) or not (AffineMap a,b) . x1 = (AffineMap a,b) . x2 or x1 = x2 )
then reconsider r1 = x1 as real number ;
assume x2 in dom (AffineMap a,b) ; :: thesis: ( not (AffineMap a,b) . x1 = (AffineMap a,b) . x2 or x1 = x2 )
then reconsider r2 = x2 as real number ;
assume (AffineMap a,b) . x1 = (AffineMap a,b) . x2 ; :: thesis: x1 = x2
then (a * r1) + b = (AffineMap a,b) . x2 by Def3
.= (a * r2) + b by Def3 ;
hence x1 = x2 by A1, XCMPLX_1:5; :: thesis: verum