begin
theorem
theorem Th2:
theorem
canceled;
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem
theorem
theorem Th10:
theorem Th11:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th18:
theorem Th19:
theorem Th20:
definition
let I be
set ;
let A be
ManySortedSet of
I;
let B,
C be
V8()
ManySortedSet of
I;
let F be
ManySortedFunction of
A,
[|B,C|];
func Mpr1 F -> ManySortedFunction of
A,
B means :
Def1:
for
i being
set st
i in I holds
it . i = pr1 (F . i);
existence
ex b1 being ManySortedFunction of A,B st
for i being set st i in I holds
b1 . i = pr1 (F . i)
uniqueness
for b1, b2 being ManySortedFunction of A,B st ( for i being set st i in I holds
b1 . i = pr1 (F . i) ) & ( for i being set st i in I holds
b2 . i = pr1 (F . i) ) holds
b1 = b2
func Mpr2 F -> ManySortedFunction of
A,
C means :
Def2:
for
i being
set st
i in I holds
it . i = pr2 (F . i);
existence
ex b1 being ManySortedFunction of A,C st
for i being set st i in I holds
b1 . i = pr2 (F . i)
uniqueness
for b1, b2 being ManySortedFunction of A,C st ( for i being set st i in I holds
b1 . i = pr2 (F . i) ) & ( for i being set st i in I holds
b2 . i = pr2 (F . i) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Mpr1 MSUALG_9:def 1 :
:: deftheorem Def2 defines Mpr2 MSUALG_9:def 2 :
theorem
theorem
theorem
theorem
begin
theorem Th25:
theorem Th26:
theorem
begin
theorem
theorem
theorem
theorem Th31:
theorem Th32:
theorem
theorem
Lm1:
now
let S be non
empty non
void ManySortedSign ;
for A being non-empty MSAlgebra of S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) holds
G is "onto" let A be
non-empty MSAlgebra of
S;
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) holds
G is "onto" let C1,
C2 be
MSCongruence of
A;
for G being ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) holds
G is "onto" let G be
ManySortedFunction of
(QuotMSAlg A,C1),
(QuotMSAlg A,C2);
( ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) implies G is "onto" )assume A1:
for
i being
Element of
S for
x being
Element of the
Sorts of
(QuotMSAlg A,C1) . i for
xx being
Element of the
Sorts of
A . i st
x = Class C1,
xx holds
(G . i) . x = Class C2,
xx
;
G is "onto" thus
G is
"onto"
verum
proof
let i be
set ;
MSUALG_3:def 3 ( not i in the carrier of S or proj2 (G . i) = the Sorts of (QuotMSAlg A,C2) . i )
set sL = the
Sorts of
(QuotMSAlg A,C1);
set sP = the
Sorts of
(QuotMSAlg A,C2);
assume
i in the
carrier of
S
;
proj2 (G . i) = the Sorts of (QuotMSAlg A,C2) . i
then reconsider s =
i as
SortSymbol of
S ;
A2:
dom (G . s) = the
Sorts of
(QuotMSAlg A,C1) . s
by FUNCT_2:def 1;
rng (G . s) c= the
Sorts of
(QuotMSAlg A,C2) . s
;
hence
rng (G . i) c= the
Sorts of
(QuotMSAlg A,C2) . i
;
XBOOLE_0:def 10 the Sorts of (QuotMSAlg A,C2) . i c= proj2 (G . i)
let q be
set ;
TARSKI:def 3 ( not q in the Sorts of (QuotMSAlg A,C2) . i or q in proj2 (G . i) )
assume
q in the
Sorts of
(QuotMSAlg A,C2) . i
;
q in proj2 (G . i)
then
q in Class (C2 . s)
by MSUALG_4:def 8;
then consider a being
set such that A3:
a in the
Sorts of
A . s
and A4:
q = Class (C2 . s),
a
by EQREL_1:def 5;
reconsider a =
a as
Element of the
Sorts of
A . s by A3;
Class (C1 . s),
a in Class (C1 . s)
by EQREL_1:def 5;
then reconsider x =
Class C1,
a as
Element of the
Sorts of
(QuotMSAlg A,C1) . s by MSUALG_4:def 8;
(G . s) . x =
Class C2,
a
by A1
.=
Class (C2 . s),
a
;
hence
q in proj2 (G . i)
by A4, A2, FUNCT_1:def 5;
verum
end;
end;
theorem Th35:
theorem Th36:
for
S being non
empty non
void ManySortedSign for
A being
non-empty MSAlgebra of
S for
C1,
C2 being
MSCongruence of
A for
G being
ManySortedFunction of
(QuotMSAlg A,C1),
(QuotMSAlg A,C2) st ( for
i being
Element of
S for
x being
Element of the
Sorts of
(QuotMSAlg A,C1) . i for
xx being
Element of the
Sorts of
A . i st
x = Class C1,
xx holds
(G . i) . x = Class C2,
xx ) holds
G is_epimorphism QuotMSAlg A,
C1,
QuotMSAlg A,
C2
theorem