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
OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2
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
OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2
let F be ManySortedFunction of U1,U2; ( F is_epimorphism U1,U2 & F is order-sorted implies OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2 )
set mc = OSCng F;
set qa = QuotOSAlg (U1,(OSCng F));
set qh = OSHomQuot F;
assume that
A1:
F is_epimorphism U1,U2
and
A2:
F is order-sorted
; OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2
set Sq = the Sorts of (QuotOSAlg (U1,(OSCng F)));
set S1 = the Sorts of U1;
set S2 = the Sorts of U2;
A3:
F is_homomorphism U1,U2
by A1;
A4:
F is "onto"
by A1;
for i being set st i in the carrier of S holds
rng ((OSHomQuot F) . i) = the Sorts of U2 . i
proof
let i be
set ;
( i in the carrier of S implies rng ((OSHomQuot F) . i) = the Sorts of U2 . i )
set f =
(OSHomQuot F) . i;
assume
i in the
carrier of
S
;
rng ((OSHomQuot F) . i) = the Sorts of U2 . i
then reconsider s =
i as
SortSymbol of
S ;
A5:
rng (F . s) = the
Sorts of
U2 . s
by A4;
A6:
(OSHomQuot F) . i = OSHomQuot (
F,
s)
by Def25;
then A7:
dom ((OSHomQuot F) . i) = the
Sorts of
(QuotOSAlg (U1,(OSCng F))) . s
by FUNCT_2:def 1;
thus
rng ((OSHomQuot F) . i) c= the
Sorts of
U2 . i
by A6, RELAT_1:def 19;
XBOOLE_0:def 10 the Sorts of U2 . i c= rng ((OSHomQuot F) . i)
let x be
object ;
TARSKI:def 3 ( not x in the Sorts of U2 . i or x in rng ((OSHomQuot F) . i) )
assume
x in the
Sorts of
U2 . i
;
x in rng ((OSHomQuot F) . i)
then consider a being
object such that A8:
a in dom (F . s)
and A9:
(F . s) . a = x
by A5, FUNCT_1:def 3;
A10:
the
Sorts of
(QuotOSAlg (U1,(OSCng F))) . s = OSClass (
(OSCng F),
s)
by Def11;
reconsider a =
a as
Element of the
Sorts of
U1 . s by A8;
((OSHomQuot F) . i) . (OSClass ((OSCng F),a)) = x
by A2, A3, A6, A9, Def24;
hence
x in rng ((OSHomQuot F) . i)
by A7, A10, FUNCT_1:def 3;
verum
end;
then A11:
OSHomQuot F is "onto"
;
OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2
by A2, A3, Th17;
then
( OSHomQuot F is_homomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is "1-1" )
;
hence
OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2
by A11, MSUALG_3:13; verum