theorem :: STACKS_1:47
for X1, X2 being StackAlgebra st X1,X2 are_isomorphic & X1 is proper-for-identity holds
X2 is proper-for-identity