let a, b, c, d, r, s be Real; :: thesis: ( a < b & b < c & c < d implies ( (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . a = 0 & (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . b = r & (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . b = r & (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . c = s & (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . c = s & (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . d = 0 ) )
assume that
A1: a < b and
A2: b < c and
A3: c < d ; :: thesis: ( (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . a = 0 & (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . b = r & (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . b = r & (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . c = s & (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . c = s & (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . d = 0 )
A4: b - a <> 0 by A1;
A5: c - b <> 0 by A2;
A6: c - d <> 0 by A3;
S1: (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . a = ((r / (b - a)) * a) + (- ((a * r) / (b - a))) by FCONT_1:def 4
.= ((a * r) / (b - a)) + (- ((a * r) / (b - a))) by XCMPLX_1:74
.= 0 ;
S2: (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . b = ((r / (b - a)) * b) + (- ((a * r) / (b - a))) by FCONT_1:def 4
.= ((r / (b - a)) * b) + ((- (a * r)) / (b - a)) by XCMPLX_1:187
.= ((r / (b - a)) * b) + (((- a) * r) / (b - a))
.= ((r / (b - a)) * b) + ((r / (b - a)) * (- a)) by XCMPLX_1:74
.= (r / (b - a)) * (b + (- a))
.= r by XCMPLX_1:87, A4 ;
S3: (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . b = (((s - r) / (c - b)) * b) + (s - ((c * (s - r)) / (c - b))) by FCONT_1:def 4
.= ((b * ((s - r) / (c - b))) + s) - ((c * (s - r)) / (c - b))
.= ((b * ((s - r) / (c - b))) + s) - (c * ((s - r) / (c - b))) by XCMPLX_1:74
.= s + (- (((- b) - (- c)) * ((s - r) / (c - b))))
.= s + (- (s - r)) by XCMPLX_1:87, A5
.= r ;
S4: (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . c = (((s - r) / (c - b)) * c) + (s - ((c * (s - r)) / (c - b))) by FCONT_1:def 4
.= ((c * (s - r)) / (c - b)) + (s - ((c * (s - r)) / (c - b))) by XCMPLX_1:74
.= s ;
S5: (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . c = (((- s) / (d - c)) * c) + (- ((d * (- s)) / (d - c))) by FCONT_1:def 4
.= (((- s) / (d - c)) * c) + ((- (d * (- s))) / (d - c)) by XCMPLX_1:187
.= (((- s) / (d - c)) * c) + (((- d) * (- s)) / (d - c))
.= (((- s) / (d - c)) * c) + (((- s) / (d - c)) * (- d)) by XCMPLX_1:74
.= ((- s) / (d - c)) * (c + (- d))
.= (s / (- (d - c))) * (c - d) by XCMPLX_1:192
.= s by A6, XCMPLX_1:87 ;
(AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . d = (((- s) / (d - c)) * d) + (- ((d * (- s)) / (d - c))) by FCONT_1:def 4
.= ((d * (- s)) / (d - c)) + (- ((d * (- s)) / (d - c))) by XCMPLX_1:74
.= 0 ;
hence ( (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . a = 0 & (AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . b = r & (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . b = r & (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . c = s & (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . c = s & (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . d = 0 ) by S1, S2, S3, S4, S5; :: thesis: verum