let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra of 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 of S; :: thesis: 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; :: thesis: ( 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;
assume
F is_epimorphism U1,U2
; :: thesis: MSHomQuot F is_isomorphism QuotMSAlg U1,(MSCng F),U2
then A1:
( F is_homomorphism U1,U2 & F is "onto" )
by MSUALG_3:def 10;
then
MSHomQuot F is_monomorphism QuotMSAlg U1,(MSCng F),U2
by Th4;
then A2:
( MSHomQuot F is_homomorphism QuotMSAlg U1,(MSCng F),U2 & MSHomQuot F is "1-1" )
by MSUALG_3:def 11;
set Sq = the Sorts of (QuotMSAlg U1,(MSCng 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 ((MSHomQuot F) . i) = the Sorts of U2 . i
proof
let i be
set ;
:: thesis: ( 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
;
:: thesis: rng ((MSHomQuot F) . i) = the Sorts of U2 . i
then reconsider s =
i as
SortSymbol of
S ;
A3:
(MSHomQuot F) . i = MSHomQuot F,
s
by Def22;
then A4:
(
dom ((MSHomQuot F) . i) = the
Sorts of
(QuotMSAlg U1,(MSCng F)) . s &
rng ((MSHomQuot F) . i) c= the
Sorts of
U2 . s )
by FUNCT_2:def 1, RELAT_1:def 19;
thus
rng ((MSHomQuot F) . i) c= the
Sorts of
U2 . i
by A3, RELAT_1:def 19;
:: according to XBOOLE_0:def 10 :: thesis: the Sorts of U2 . i c= rng ((MSHomQuot F) . i)
A5:
rng (F . s) = the
Sorts of
U2 . s
by A1, 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 ((MSHomQuot F) . i) )
assume
x in the
Sorts of
U2 . i
;
:: thesis: x in rng ((MSHomQuot F) . i)
then consider a being
set such that A6:
(
a in dom (F . s) &
(F . s) . a = x )
by A5, FUNCT_1:def 5;
reconsider a =
a as
Element of the
Sorts of
U1 . s by A6;
A7:
((MSHomQuot F) . i) . (Class (MSCng F,s),a) = x
by A1, A3, A6, Def21;
A8:
MSCng F,
s = (MSCng F) . s
by A1, Def20;
the
Sorts of
(QuotMSAlg U1,(MSCng F)) . s = Class ((MSCng F) . s)
by Def8;
then
Class (MSCng F,s),
a in dom ((MSHomQuot F) . i)
by A4, A8, EQREL_1:def 5;
hence
x in rng ((MSHomQuot F) . i)
by A7, FUNCT_1:def 5;
:: thesis: verum
end;
then
MSHomQuot F is "onto"
by MSUALG_3:def 3;
hence
MSHomQuot F is_isomorphism QuotMSAlg U1,(MSCng F),U2
by A2, MSUALG_3:13; :: thesis: verum