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