let A, B, C, D be Real; :: thesis: ( A > 0 & C > 0 implies AffineMap (A,B,C,D) is one-to-one )
assume that
A1: A > 0 and
A2: C > 0 ; :: thesis: AffineMap (A,B,C,D) is one-to-one
set ff = AffineMap (A,B,C,D);
for x1, x2 being object st x1 in dom (AffineMap (A,B,C,D)) & x2 in dom (AffineMap (A,B,C,D)) & (AffineMap (A,B,C,D)) . x1 = (AffineMap (A,B,C,D)) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom (AffineMap (A,B,C,D)) & x2 in dom (AffineMap (A,B,C,D)) & (AffineMap (A,B,C,D)) . x1 = (AffineMap (A,B,C,D)) . x2 implies x1 = x2 )
assume that
A3: x1 in dom (AffineMap (A,B,C,D)) and
A4: x2 in dom (AffineMap (A,B,C,D)) and
A5: (AffineMap (A,B,C,D)) . x1 = (AffineMap (A,B,C,D)) . x2 ; :: thesis: x1 = x2
reconsider p2 = x2 as Point of (TOP-REAL 2) by A4;
reconsider p1 = x1 as Point of (TOP-REAL 2) by A3;
A6: ( (AffineMap (A,B,C,D)) . x1 = |[((A * (p1 `1)) + B),((C * (p1 `2)) + D)]| & (AffineMap (A,B,C,D)) . x2 = |[((A * (p2 `1)) + B),((C * (p2 `2)) + D)]| ) by Def2;
then (A * (p1 `1)) + B = (A * (p2 `1)) + B by A5, SPPOL_2:1;
then p1 `1 = (A * (p2 `1)) / A by A1, XCMPLX_1:89;
then A7: p1 `1 = p2 `1 by A1, XCMPLX_1:89;
(C * (p1 `2)) + D = (C * (p2 `2)) + D by A5, A6, SPPOL_2:1;
then p1 `2 = (C * (p2 `2)) / C by A2, XCMPLX_1:89;
hence x1 = x2 by A2, A7, TOPREAL3:6, XCMPLX_1:89; :: thesis: verum

end;

hence AffineMap (A,B,C,D) is one-to-one by FUNCT_1:def 4; :: thesis: verum