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, MSUALG_3:def 10;
A4:
F is "onto"
by A1, MSUALG_3:def 10;
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, MSUALG_3:def 3;
A6:
(OSHomQuot F) . i = OSHomQuot F,
s
by Def27;
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
set ;
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
set such that A8:
a in dom (F . s)
and A9:
(F . s) . a = x
by A5, FUNCT_1:def 5;
A10:
the
Sorts of
(QuotOSAlg U1,(OSCng F)) . s = OSClass (OSCng F),
s
by Def13;
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, Def26;
hence
x in rng ((OSHomQuot F) . i)
by A7, A10, FUNCT_1:def 5;
verum
end;
then A11:
OSHomQuot F is "onto"
by MSUALG_3:def 3;
OSHomQuot F is_monomorphism QuotOSAlg U1,(OSCng F),U2
by A2, A3, Th18;
then
( OSHomQuot F is_homomorphism QuotOSAlg U1,(OSCng F),U2 & OSHomQuot F is "1-1" )
by MSUALG_3:def 11;
hence
OSHomQuot F is_isomorphism QuotOSAlg U1,(OSCng F),U2
by A11, MSUALG_3:13; verum