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