theorem :: MATHMORP:66

for t being Real
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)