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

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