theorem :: PZFMISC1:64

for I being set
for x1, x2, A, B being ManySortedSet of I holds [|(x1 (\/) x2),(A (\/) B)|] = (([|x1,A|] (\/) [|x1,B|]) (\/) [|x2,A|]) (\/) [|x2,B|]