let a, b, x be Real; ( 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
; 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; verum