let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
QuotMSAlg U1,(MSCng F),U2 are_isomorphic
let U1, U2 be non-empty MSAlgebra of S; :: thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
QuotMSAlg U1,(MSCng F),U2 are_isomorphic
let F be ManySortedFunction of U1,U2; :: thesis: ( F is_epimorphism U1,U2 implies QuotMSAlg U1,(MSCng F),U2 are_isomorphic )
assume F is_epimorphism U1,U2 ; :: thesis: QuotMSAlg U1,(MSCng F),U2 are_isomorphic
then MSHomQuot F is_isomorphism QuotMSAlg U1,(MSCng F),U2 by Th5;
hence QuotMSAlg U1,(MSCng F),U2 are_isomorphic by MSUALG_3:def 13; :: thesis: verum