theorem :: STACKS_1:42

for X being StackAlgebra holds id the carrier of X, id the carrier' of X form_isomorphism_between X,X ;