let S be non empty non void ManySortedSign ; for U1 being non-empty MSAlgebra of S
for R being MSCongruence of U1 holds MSNat_Hom U1,R is_epimorphism U1, QuotMSAlg U1,R
let U1 be non-empty MSAlgebra of S; for R being MSCongruence of U1 holds MSNat_Hom U1,R is_epimorphism U1, QuotMSAlg U1,R
let R be MSCongruence of U1; MSNat_Hom U1,R is_epimorphism U1, QuotMSAlg U1,R
set F = MSNat_Hom U1,R;
set QA = QuotMSAlg U1,R;
set S1 = the Sorts of U1;
for o being OperSymbol of S st Args o,U1 <> {} holds
for x being Element of Args o,U1 holds ((MSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(QuotMSAlg U1,R)) . ((MSNat_Hom U1,R) # x)
proof
let o be
OperSymbol of
S;
( Args o,U1 <> {} implies for x being Element of Args o,U1 holds ((MSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(QuotMSAlg U1,R)) . ((MSNat_Hom U1,R) # x) )
assume
Args o,
U1 <> {}
;
for x being Element of Args o,U1 holds ((MSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(QuotMSAlg U1,R)) . ((MSNat_Hom U1,R) # x)
let x be
Element of
Args o,
U1;
((MSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(QuotMSAlg U1,R)) . ((MSNat_Hom U1,R) # x)
set ro =
the_result_sort_of o;
set ar =
the_arity_of o;
the
Arity of
S . o = the_arity_of o
by MSUALG_1:def 6;
then A1:
(((Class R) # ) * the Arity of S) . o = product ((Class R) * (the_arity_of o))
by MSAFREE:1;
A2:
dom x = dom (the_arity_of o)
by MSUALG_3:6;
A3:
for
a being
set st
a in dom (the_arity_of o) holds
((MSNat_Hom U1,R) # x) . a = (R # x) . a
proof
let a be
set ;
( a in dom (the_arity_of o) implies ((MSNat_Hom U1,R) # x) . a = (R # x) . a )
assume A4:
a in dom (the_arity_of o)
;
((MSNat_Hom U1,R) # x) . a = (R # x) . a
then reconsider n =
a as
Nat by ORDINAL1:def 13;
set Fo =
MSNat_Hom U1,
R,
((the_arity_of o) /. n);
set s =
(the_arity_of o) /. n;
A5:
n in dom (the Sorts of U1 * (the_arity_of o))
by A4, PARTFUN1:def 4;
then (the Sorts of U1 * (the_arity_of o)) . n =
the
Sorts of
U1 . ((the_arity_of o) . n)
by FUNCT_1:22
.=
the
Sorts of
U1 . ((the_arity_of o) /. n)
by A4, PARTFUN1:def 8
;
then reconsider xn =
x . n as
Element of the
Sorts of
U1 . ((the_arity_of o) /. n) by A5, MSUALG_3:6;
thus ((MSNat_Hom U1,R) # x) . a =
((MSNat_Hom U1,R) . ((the_arity_of o) /. n)) . (x . n)
by A2, A4, MSUALG_3:def 8
.=
(MSNat_Hom U1,R,((the_arity_of o) /. n)) . xn
by Def18
.=
Class (R . ((the_arity_of o) /. n)),
(x . n)
by Def17
.=
(R # x) . a
by A4, Def9
;
verum
end;
dom the
Sorts of
U1 = the
carrier of
S
by PARTFUN1:def 4;
then
rng the
ResultSort of
S c= dom the
Sorts of
U1
;
then
(
dom the
ResultSort of
S = the
carrier' of
S &
dom (the Sorts of U1 * the ResultSort of S) = dom the
ResultSort of
S )
by FUNCT_2:def 1, RELAT_1:46;
then A6:
(the Sorts of U1 * the ResultSort of S) . o =
the
Sorts of
U1 . (the ResultSort of S . o)
by FUNCT_1:22
.=
the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 7
;
then reconsider dx =
(Den o,U1) . x as
Element of the
Sorts of
U1 . (the_result_sort_of o) by MSUALG_1:def 10;
(
rng (Den o,U1) c= Result o,
U1 &
Result o,
U1 = the
Sorts of
U1 . (the_result_sort_of o) )
by A6, MSUALG_1:def 10;
then
rng (Den o,U1) c= dom (QuotRes R,o)
by A6, FUNCT_2:def 1;
then A7:
(
dom (Den o,U1) = Args o,
U1 &
dom ((QuotRes R,o) * (Den o,U1)) = dom (Den o,U1) )
by FUNCT_2:def 1, RELAT_1:46;
dom (Class R) = the
carrier of
S
by PARTFUN1:def 4;
then
(
dom (R # x) = dom ((Class R) * (the_arity_of o)) &
rng (the_arity_of o) c= dom (Class R) )
by CARD_3:18;
then
(
dom ((MSNat_Hom U1,R) # x) = dom (the_arity_of o) &
dom (R # x) = dom (the_arity_of o) )
by MSUALG_3:6, RELAT_1:46;
then A8:
(MSNat_Hom U1,R) # x = R # x
by A3, FUNCT_1:9;
Den o,
(QuotMSAlg U1,R) =
(QuotCharact R) . o
by MSUALG_1:def 11
.=
QuotCharact R,
o
by Def15
;
then (Den o,(QuotMSAlg U1,R)) . ((MSNat_Hom U1,R) # x) =
((QuotRes R,o) * (Den o,U1)) . x
by A1, A8, Def14
.=
(QuotRes R,o) . dx
by A7, FUNCT_1:22
.=
Class R,
dx
by Def10
.=
(MSNat_Hom U1,R,(the_result_sort_of o)) . dx
by Def17
.=
((MSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x)
by Def18
;
hence
((MSNat_Hom U1,R) . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(QuotMSAlg U1,R)) . ((MSNat_Hom U1,R) # x)
;
verum
end;
hence
MSNat_Hom U1,R is_homomorphism U1, QuotMSAlg U1,R
by MSUALG_3:def 9; MSUALG_3:def 10 MSNat_Hom U1,R is "onto"
for i being set st i in the carrier of S holds
rng ((MSNat_Hom U1,R) . i) = the Sorts of (QuotMSAlg U1,R) . i
proof
let i be
set ;
( i in the carrier of S implies rng ((MSNat_Hom U1,R) . i) = the Sorts of (QuotMSAlg U1,R) . i )
assume
i in the
carrier of
S
;
rng ((MSNat_Hom U1,R) . i) = the Sorts of (QuotMSAlg U1,R) . i
then reconsider s =
i as
Element of
S ;
reconsider f =
(MSNat_Hom U1,R) . i as
Function of
(the Sorts of U1 . s),
(the Sorts of (QuotMSAlg U1,R) . s) by PBOOLE:def 18;
A9:
dom f = the
Sorts of
U1 . s
by FUNCT_2:def 1;
A10:
the
Sorts of
(QuotMSAlg U1,R) . s = Class (R . s)
by Def8;
for
x being
set st
x in the
Sorts of
(QuotMSAlg U1,R) . i holds
x in rng f
proof
let x be
set ;
( x in the Sorts of (QuotMSAlg U1,R) . i implies x in rng f )
A11:
f = MSNat_Hom U1,
R,
s
by Def18;
assume
x in the
Sorts of
(QuotMSAlg U1,R) . i
;
x in rng f
then consider a1 being
set such that A12:
a1 in the
Sorts of
U1 . s
and A13:
x = Class (R . s),
a1
by A10, EQREL_1:def 5;
f . a1 in rng f
by A9, A12, FUNCT_1:def 5;
hence
x in rng f
by A12, A13, A11, Def17;
verum
end;
then
the
Sorts of
(QuotMSAlg U1,R) . i c= rng f
by TARSKI:def 3;
hence
rng ((MSNat_Hom U1,R) . i) = the
Sorts of
(QuotMSAlg U1,R) . i
by XBOOLE_0:def 10;
verum
end;
hence
MSNat_Hom U1,R is "onto"
by MSUALG_3:def 3; verum