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