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 JORDAN16:def 3
.= (((a * x0) + b) - ((a * x1) + b)) / (x0 - x1) by JORDAN16:def 3
.= (a * (x0 - x1)) / (x0 - x1) ;
hence [!(AffineMap a,b),x0,x1!] = a by A1, XCMPLX_1:90; :: thesis: verum