theorem Th96: :: ZFMISC_1:97

for X, Y, Z being set holds
( [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] & [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] )