theorem :: FUNCT_4:22

for X, Y being set holds (id X) +* (id Y) = id (X \/ Y)