theorem Th1: :: NECKLA_3:1

for A, B being set holds (id A) | B = (id A) /\ [:B,B:]