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