A27: 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 b₁ being Function of T,(TOP-REAL n) st b₁ = f <##> g holds
b₁ is continuous by A27; :: thesis: verum