let S be non empty non void ManySortedSign ; for U1, U2 being non-empty MSAlgebra over 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 over S; 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; ( F is_epimorphism U1,U2 implies QuotMSAlg (U1,(MSCng F)),U2 are_isomorphic )
assume
F is_epimorphism U1,U2
; 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
; verum