theorem Th82: :: MEMBER_1:82

for F, G, H being ext-real-membered set holds F ** (G \/ H) = (F ** G) \/ (F ** H)