A1: ex H being ManySortedFunction of F₂(),F₃() st H is_epimorphism F₂(),F₃() and
A2: P₁[F₂()] and
A3: for A, B being non-empty MSAlgebra over F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A4: for A being non-empty MSAlgebra over F₁()
for R being MSCongruence of A st P₁[A] holds
P₁[ QuotMSAlg (A,R)]