consider H being ManySortedFunction of F₂(),F₃() such that
A5: H is_epimorphism F₂(),F₃() by A1;
P₁[ QuotMSAlg (F₂(),(MSCng H))] by A2, A4;
hence P₁[F₃()] by A3, A5, MSUALG_4:6; :: thesis: verum