set f = AffineMap (a,b);
for x0 being Real st x0 in REAL holds
(AffineMap (a,b)) . x0 = (a * x0) + b by Def4;
then ( REAL = dom (AffineMap (a,b)) & (AffineMap (a,b)) | REAL is continuous ) by Th41, FUNCT_2:def 1;
hence AffineMap (a,b) is continuous ; :: thesis: verum