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