let p, q, s, t be Real; :: thesis: ( s <> p implies ( (AffineMap (p,q)) . ((t - q) / (p - s)) = (AffineMap (s,t)) . ((t - q) / (p - s)) & (AffineMap (s,t)) . ((t - q) / (p - s)) = ((p * t) - (q * s)) / (p - s) ) )
assume s <> p ; :: thesis: ( (AffineMap (p,q)) . ((t - q) / (p - s)) = (AffineMap (s,t)) . ((t - q) / (p - s)) & (AffineMap (s,t)) . ((t - q) / (p - s)) = ((p * t) - (q * s)) / (p - s) )
then A1: p - s <> 0 ;
A2: (AffineMap (s,t)) . ((t - q) / (p - s)) = (s * ((t - q) / (p - s))) + t by FCONT_1:def 4
.= ((s * (t - q)) / (p - s)) + t by XCMPLX_1:74
.= ((s * (t - q)) / (p - s)) + (t * ((p - s) / (p - s))) by XCMPLX_1:88, A1
.= ((s * (t - q)) / (p - s)) + ((t * (p - s)) / (p - s)) by XCMPLX_1:74
.= ((s * (t - q)) + (t * (p - s))) / (p - s) by XCMPLX_1:62
.= ((((s * t) - (s * q)) + (t * p)) - (t * s)) / (p - s) ;
(AffineMap (p,q)) . ((t - q) / (p - s)) = (p * ((t - q) / (p - s))) + q by FCONT_1:def 4
.= ((p * (t - q)) / (p - s)) + q by XCMPLX_1:74
.= ((p * (t - q)) / (p - s)) + (q * ((p - s) / (p - s))) by XCMPLX_1:88, A1
.= ((p * (t - q)) / (p - s)) + ((q * (p - s)) / (p - s)) by XCMPLX_1:74
.= ((p * (t - q)) + (q * (p - s))) / (p - s) by XCMPLX_1:62
.= ((((p * t) - (p * q)) + (q * p)) - (q * s)) / (p - s) ;
hence ( (AffineMap (p,q)) . ((t - q) / (p - s)) = (AffineMap (s,t)) . ((t - q) / (p - s)) & (AffineMap (s,t)) . ((t - q) / (p - s)) = ((p * t) - (q * s)) / (p - s) ) by A2; :: thesis: verum