let x0, x1, a, b be Real; :: thesis: ( x0 <> x1 implies [!(AffineMap (a,b)),x0,x1!] = a )
assume x0 <> x1 ; :: thesis: [!(AffineMap (a,b)),x0,x1!] = a
then A1: x0 - x1 <> 0 ;
[!(AffineMap (a,b)),x0,x1!] = (((a * x0) + b) - ((AffineMap (a,b)) . x1)) / (x0 - x1) by FCONT_1:def 4
.= (((a * x0) + b) - ((a * x1) + b)) / (x0 - x1) by FCONT_1:def 4
.= (a * (x0 - x1)) / (x0 - x1) ;
hence [!(AffineMap (a,b)),x0,x1!] = a by A1, XCMPLX_1:89; :: thesis: verum