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