theorem Th54: :: TOPREALC:54

for n being Nat
for T being non empty TopSpace
for f, g being Function of T,(TOP-REAL n) holds f <##> g = (TIMES n) .: (f,g)