let a, b, x, y be Real; :: 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:68;
( (AffineMap (a,b)) . x = (a * x) + b & (AffineMap (a,b)) . y = (a * y) + b ) by Def4;
hence (AffineMap (a,b)) . x < (AffineMap (a,b)) . y by A1, XREAL_1:8; :: thesis: verum