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