let b, a be Real; :: thesis: (AffineMap (0,b)) . a = b
(AffineMap (0,b)) . a = (0 * a) + b by FCONT_1:def 4
.= b ;
hence (AffineMap (0,b)) . a = b ; :: thesis: verum