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