In this paper, some important theories of structured object calculus using the results contributed by Goguen are proved. These theories ensure to build up the description of new objects from the description of the existing objects and verify the global system with theories deduced from existing objects as lemma. In addition, the object reification on the basis of object encapsulation is studied, and a structured object calculus is achieved.