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