theorem Th39: :: XTUPLE_0:39

for X, Y being set holds proj1_4 (X \/ Y) = (proj1_4 X) \/ (proj1_4 Y)