@MISC{BIRKHOFF.MIZ,
  AUTHOR = {Korni{\l}owicz, Artur},
  TITLE = {{B}irkhoff Theorem for Many Sorted Algebras},
  DAY = {19},
  MONTH = {June},
  YEAR = {1997},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = { \newcommand \pred[1]{${\cal P} #1$}
In this article Birkhoff Variety Theorem for many sorted algebras is proved.
A class of algebras is represented by predicate \pred{}. Notation \pred{[A]},
where $A$ is an algebra, means that $A$ is in class \pred{}.
All algebras in our class are many sorted over many sorted signature $S$.
The properties of varieties:
 \begin{itemize} \itemsep-3pt
 \item a class \pred{ } of algebras is abstract
 \item a class \pred{ } of algebras is closed under subalgebras
 \item a class \pred{ } of algebras is closed under congruences
 \item a class \pred{ } of algebras is closed under products
 \end{itemize}
 are published in this paper as:
 \begin{itemize} \itemsep-3pt
 \item for all non-empty algebras $A$, $B$ over $S$ such that $A$ and $B$
   are\_isomorphic and \pred{[A]} holds \pred{[B]}
 \item for every non-empty algebra $A$ over $S$
  and for strict non-empty subalgebra $B$ of $A$ such that \pred{[A]}
  holds \pred{[B]}
 \item for every non-empty algebra $A$ over $S$ and
  for every congruence $R$ of $A$ such that \pred{[A]} holds \pred{[A\slash R]}
 \item Let $I$ be a set and $F$
be an algebra family of $I$ over ${\cal A}.$
Suppose that for every set $i$                                        
such that $i \in I$
there exists an algebra $A$
over ${\cal A}$
such that $A = F(i)$
 and ${\cal P}[A]$.
Then${\cal P}[\prod F]$.
 \end{itemize}
This paper is formalization of parts of \cite{WECHLER}.}}

