A25: f <##> g = (TIMES n) .: (f,g) by Th54;
<:f,g:> is continuous Function of T,[:(TOP-REAL n),(TOP-REAL n):] by YELLOW12:41;
hence for b1 being Function of T,(TOP-REAL n) st b1 = f <##> g holds
b1 is continuous by A25; :: thesis: verum