let a, b be real number ; :: thesis: (AffineMap a,b) . 1 = a + b
thus (AffineMap a,b) . 1 = (a * 1) + b by Def3
.= a + b ; :: thesis: verum