let a, b, x, y be real number ; :: thesis: ( a > 0 & x < y implies (AffineMap a,b) . x < (AffineMap a,b) . y )
assume ( a > 0 & x < y ) ; :: thesis: (AffineMap a,b) . x < (AffineMap a,b) . y
then A1: a * x < a * y by XREAL_1:70;
( (AffineMap a,b) . x = (a * x) + b & (AffineMap a,b) . y = (a * y) + b ) by Def3;
hence (AffineMap a,b) . x < (AffineMap a,b) . y by A1, XREAL_1:10; :: thesis: verum