set f = AffineMap a,b;
A1: REAL = dom (AffineMap a,b) by FUNCT_2:def 1;
for x0 being real number st x0 in REAL holds
(AffineMap a,b) . x0 = (a * x0) + b by Def3;
then (AffineMap a,b) | REAL is continuous by FCONT_1:48;
hence AffineMap a,b is continuous by A1, RELAT_1:98; :: thesis: verum