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
OSHomQuot F is_isomorphism QuotOSAlg U1,(OSCng F),U2
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
OSHomQuot F is_isomorphism QuotOSAlg U1,(OSCng F),U2
let F be ManySortedFunction of U1,U2; :: thesis: ( 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 A1:
( F is_epimorphism U1,U2 & F is order-sorted )
; :: thesis: OSHomQuot F is_isomorphism QuotOSAlg U1,(OSCng F),U2
then A2:
( F is_homomorphism U1,U2 & F is "onto" )
by MSUALG_3:def 10;
then
OSHomQuot F is_monomorphism QuotOSAlg U1,(OSCng F),U2
by A1, Th18;
then A3:
( OSHomQuot F is_homomorphism QuotOSAlg U1,(OSCng F),U2 & OSHomQuot F is "1-1" )
by MSUALG_3:def 11;
set Sq = the Sorts of (QuotOSAlg U1,(OSCng F));
set S1 = the Sorts of U1;
set S2 = the Sorts of U2;
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 ;
:: thesis: ( 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
;
:: thesis: rng ((OSHomQuot F) . i) = the Sorts of U2 . i
then reconsider s =
i as
SortSymbol of
S ;
A4:
(OSHomQuot F) . i = OSHomQuot F,
s
by Def27;
then A5:
(
dom ((OSHomQuot F) . i) = the
Sorts of
(QuotOSAlg U1,(OSCng F)) . s &
rng ((OSHomQuot F) . i) c= the
Sorts of
U2 . s )
by FUNCT_2:def 1, RELAT_1:def 19;
thus
rng ((OSHomQuot F) . i) c= the
Sorts of
U2 . i
by A4, RELAT_1:def 19;
:: according to XBOOLE_0:def 10 :: thesis: the Sorts of U2 . i c= rng ((OSHomQuot F) . i)
A6:
rng (F . s) = the
Sorts of
U2 . s
by A2, MSUALG_3:def 3;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of U2 . i or x in rng ((OSHomQuot F) . i) )
assume
x in the
Sorts of
U2 . i
;
:: thesis: x in rng ((OSHomQuot F) . i)
then consider a being
set such that A7:
(
a in dom (F . s) &
(F . s) . a = x )
by A6, FUNCT_1:def 5;
reconsider a =
a as
Element of the
Sorts of
U1 . s by A7;
A8:
((OSHomQuot F) . i) . (OSClass (OSCng F),a) = x
by A1, A2, A4, A7, Def26;
the
Sorts of
(QuotOSAlg U1,(OSCng F)) . s = OSClass (OSCng F),
s
by Def13;
hence
x in rng ((OSHomQuot F) . i)
by A5, A8, FUNCT_1:def 5;
:: thesis: verum
end;
then
OSHomQuot F is "onto"
by MSUALG_3:def 3;
hence
OSHomQuot F is_isomorphism QuotOSAlg U1,(OSCng F),U2
by A3, MSUALG_3:13; :: thesis: verum