let S be locally_directed OrderSortedSign; 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; 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; ( 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 )
; QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic
then
OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2
by Th18;
hence
QuotOSAlg (U1,(OSCng F)),U2 are_isomorphic
; verum