theorem Th60: :: MATHMORP:60

for t, s being Real
for n being Element of NAT
for X being Subset of (TOP-REAL n) holds (t * s) (.) X = t (.) (s (.) X)