let a, b be Real; :: 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 object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (AffineMap (a,b)) or not x2 in dom (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 dom (AffineMap (a,b)) or not (AffineMap (a,b)) . x1 = (AffineMap (a,b)) . x2 or x1 = x2 )

then reconsider r1 = x1 as Real ;

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 ;

assume (AffineMap (a,b)) . x1 = (AffineMap (a,b)) . x2 ; :: thesis: x1 = x2

then (a * r1) + b = (AffineMap (a,b)) . x2 by Def4

.= (a * r2) + b by Def4 ;

hence x1 = x2 by A1, XCMPLX_1:5; :: thesis: verum

assume A1: a <> 0 ; :: thesis: AffineMap (a,b) is one-to-one

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (AffineMap (a,b)) or not x2 in dom (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 dom (AffineMap (a,b)) or not (AffineMap (a,b)) . x1 = (AffineMap (a,b)) . x2 or x1 = x2 )

then reconsider r1 = x1 as Real ;

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 ;

assume (AffineMap (a,b)) . x1 = (AffineMap (a,b)) . x2 ; :: thesis: x1 = x2

then (a * r1) + b = (AffineMap (a,b)) . x2 by Def4

.= (a * r2) + b by Def4 ;

hence x1 = x2 by A1, XCMPLX_1:5; :: thesis: verum