let o, m be set ; :: thesis: IdCat (1Cat (o,m)) = 1Cat (o,m)
1Cat (o,m) is discrete by Th39;
hence IdCat (1Cat (o,m)) = 1Cat (o,m) by Th45; :: thesis: verum