A1: P₂[F₂()] and
A2: P₁[F₃()] and
A3: for C being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of C st P₂[C] holds
ex h being ManySortedFunction of F₃(),C st
( h is_homomorphism F₃(),C & G = h ** F₄() ) and
A4: for A, B being non-empty MSAlgebra over F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A5: for A being non-empty MSAlgebra over F₁()
for R being MSCongruence of A st P₁[A] holds
P₁[ QuotMSAlg (A,R)]