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