let S be non empty non void ManySortedSign ; for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2
let U1, U2 be non-empty MSAlgebra over S; for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2
let F be ManySortedFunction of U1,U2; ( F is_epimorphism U1,U2 implies MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2 )
set mc = MSCng F;
set qa = QuotMSAlg (U1,(MSCng F));
set qh = MSHomQuot F;
set Sq = the Sorts of (QuotMSAlg (U1,(MSCng F)));
set S1 = the Sorts of U1;
set S2 = the Sorts of U2;
assume A1:
F is_epimorphism U1,U2
; MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2
then A2:
F is_homomorphism U1,U2
;
A3:
F is "onto"
by A1;
for i being set st i in the carrier of S holds
rng ((MSHomQuot F) . i) = the Sorts of U2 . i
proof
let i be
set ;
( i in the carrier of S implies rng ((MSHomQuot F) . i) = the Sorts of U2 . i )
set f =
(MSHomQuot F) . i;
assume
i in the
carrier of
S
;
rng ((MSHomQuot F) . i) = the Sorts of U2 . i
then reconsider s =
i as
SortSymbol of
S ;
A4:
rng (F . s) = the
Sorts of
U2 . s
by A3;
A5:
(MSHomQuot F) . i = MSHomQuot (
F,
s)
by Def20;
hence
rng ((MSHomQuot F) . i) c= the
Sorts of
U2 . i
by RELAT_1:def 19;
XBOOLE_0:def 10 the Sorts of U2 . i c= rng ((MSHomQuot F) . i)
let x be
object ;
TARSKI:def 3 ( not x in the Sorts of U2 . i or x in rng ((MSHomQuot F) . i) )
assume
x in the
Sorts of
U2 . i
;
x in rng ((MSHomQuot F) . i)
then consider a being
object such that A6:
a in dom (F . s)
and A7:
(F . s) . a = x
by A4, FUNCT_1:def 3;
A8:
(
MSCng (
F,
s)
= (MSCng F) . s & the
Sorts of
(QuotMSAlg (U1,(MSCng F))) . s = Class ((MSCng F) . s) )
by A2, Def6, Def18;
reconsider a =
a as
Element of the
Sorts of
U1 . s by A6;
dom ((MSHomQuot F) . i) = the
Sorts of
(QuotMSAlg (U1,(MSCng F))) . s
by A5, FUNCT_2:def 1;
then A9:
Class (
(MSCng (F,s)),
a)
in dom ((MSHomQuot F) . i)
by A8, EQREL_1:def 3;
((MSHomQuot F) . i) . (Class ((MSCng (F,s)),a)) = x
by A2, A5, A7, Def19;
hence
x in rng ((MSHomQuot F) . i)
by A9, FUNCT_1:def 3;
verum
end;
then A10:
MSHomQuot F is "onto"
;
MSHomQuot F is_monomorphism QuotMSAlg (U1,(MSCng F)),U2
by A2, Th4;
then
( MSHomQuot F is_homomorphism QuotMSAlg (U1,(MSCng F)),U2 & MSHomQuot F is "1-1" )
;
hence
MSHomQuot F is_isomorphism QuotMSAlg (U1,(MSCng F)),U2
by A10, MSUALG_3:13; verum