let a, b be Real; :: thesis: (AffineMap (a,b)) . 1 = a + b
thus (AffineMap (a,b)) . 1 = (a * 1) + b by Def4
.= a + b ; :: thesis: verum