theorem :: FUNCTOR1:17

for A being non empty transitive with_units AltCatStr holds (id A) " = id A