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