let a, b, c, r be Real; :: thesis: ( a < b & b < c implies (r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) . b = (r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) . b )
set fa = r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))));
set fc = r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))));
assume ( a < b & b < c ) ; :: thesis: (r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) . b = (r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) . b
then A7: ( b - a <> 0 & c - b <> 0 ) ;
thus (r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) . b = r * ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) . b) by VALUED_1:6
.= r * (((1 / (b - a)) * b) + (- (a / (b - a)))) by FCONT_1:def 4
.= r * (((1 / (b - a)) * b) - (a / (b - a)))
.= r * ((b / (b - a)) - (a / (b - a))) by XCMPLX_1:99
.= r * ((b - a) / (b - a)) by XCMPLX_1:120
.= r * 1 by XCMPLX_1:60, A7
.= r * ((c - b) / (c - b)) by XCMPLX_1:60, A7
.= r * ((c / (c - b)) - (b / (c - b))) by XCMPLX_1:120
.= r * ((c / (c - b)) - ((1 / (c - b)) * b)) by XCMPLX_1:99
.= r * (((- (1 / (c - b))) * b) + (c / (c - b)))
.= r * ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b) by FCONT_1:def 4
.= (r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) . b by VALUED_1:6 ; :: thesis: verum