let a, b, p, q be Real; :: thesis: ( a <> p implies (AffineMap (a,b)) . ((q - b) / (a - p)) = (AffineMap (p,q)) . ((q - b) / (a - p)) )
assume a <> p ; :: thesis: (AffineMap (a,b)) . ((q - b) / (a - p)) = (AffineMap (p,q)) . ((q - b) / (a - p))
then B1: a - p <> 0 ;
B2: (AffineMap (a,b)) . ((q - b) / (a - p)) = (a * ((q - b) / (a - p))) + b by FCONT_1:def 4
.= ((a * (q - b)) / (a - p)) + b by XCMPLX_1:74
.= ((a * (q - b)) + ((a - p) * b)) / (a - p) by XCMPLX_1:113, B1 ;
(AffineMap (p,q)) . ((q - b) / (a - p)) = (p * ((q - b) / (a - p))) + q by FCONT_1:def 4
.= ((p * (q - b)) / (a - p)) + q by XCMPLX_1:74
.= ((p * (q - b)) + ((a - p) * q)) / (a - p) by XCMPLX_1:113, B1 ;
hence (AffineMap (a,b)) . ((q - b) / (a - p)) = (AffineMap (p,q)) . ((q - b) / (a - p)) by B2; :: thesis: verum