let S be locally_directed OrderSortedSign; :: thesis: for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds
QuotOSAlg U1,(OSCng F),U2 are_isomorphic
let U1, U2 be non-empty OSAlgebra of S; :: thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 & F is order-sorted holds
QuotOSAlg U1,(OSCng F),U2 are_isomorphic
let F be ManySortedFunction of U1,U2; :: thesis: ( F is_epimorphism U1,U2 & F is order-sorted implies QuotOSAlg U1,(OSCng F),U2 are_isomorphic )
assume ( F is_epimorphism U1,U2 & F is order-sorted ) ; :: thesis: QuotOSAlg U1,(OSCng F),U2 are_isomorphic
then OSHomQuot F is_isomorphism QuotOSAlg U1,(OSCng F),U2 by Th19;
hence QuotOSAlg U1,(OSCng F),U2 are_isomorphic by MSUALG_3:def 13; :: thesis: verum