let a, b, x be Real; :: thesis: ( b - a <> 0 & (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x = 1 implies x = b )
assume that
A0: b - a <> 0 and
A1: (AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x = 1 ; :: thesis: x = b
( x in REAL & b in REAL ) by XREAL_0:def 1;
then A3: ( x in dom (AffineMap ((1 / (b - a)),(- (a / (b - a))))) & b in dom (AffineMap ((1 / (b - a)),(- (a / (b - a))))) ) by FUNCT_2:def 1;
(AffineMap ((1 / (b - a)),(- (a / (b - a))))) . b = 1 by A0, Ab1;
hence x = b by A1, FUNCT_1:def 4, A3, A0; :: thesis: verum