let b, c be Real; :: thesis: ( c - b <> 0 implies (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b = 1 )
assume A1: c - b <> 0 ; :: thesis: (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b = 1
(AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b = ((- (1 / (c - b))) * b) + (c / (c - b)) by FCONT_1:def 4
.= (((- 1) / (c - b)) * b) + (c / (c - b)) by XCMPLX_1:187
.= (((- 1) * b) / (c - b)) + (c / (c - b)) by XCMPLX_1:74
.= ((- b) + c) / (c - b) by XCMPLX_1:62
.= 1 by A1, XCMPLX_1:60 ;
hence (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b = 1 ; :: thesis: verum