theorem Th191: :: MEMBER_1:191

for F, G being ext-real-membered set
for r being Real st r <> 0 holds
r ** (F \ G) = (r ** F) \ (r ** G)