let A, B, C, D be real number ; :: 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 set 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 set ; :: 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:90;
then A7: p1 `1 = p2 `1 by A1, XCMPLX_1:90;
(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:90;
hence x1 = x2 by A2, A7, TOPREAL3:11, XCMPLX_1:90; :: thesis: verum

end;

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