theorem Thm25: :: SRINGS_4:26
for x, y being set holds (product <*x*>) /\ (product <*y*>) = product <*(x /\ y)*>