theorem Th64: :: MATHMORP:64

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 (-) Y) = (t (.) X) (-) (t (.) Y)