Copyright (c) 1996 Association of Mizar Users
environ
vocabulary AMI_1, MSUALG_1, PBOOLE, FUNCT_1, PRE_CIRC, CLOSURE2, CAT_4,
MSUALG_2, ZF_REFLE, FINSET_1, FINSEQ_1, RELAT_1, QC_LANG1, PRALG_2,
CARD_3, RLVECT_2, MSAFREE, PRELAMB, PRALG_1, FUNCT_3, MCART_1, EQREL_1,
FUNCOP_1, BOOLE, MSUALG_3, TREES_4, LANG1, BORSUK_1, ALG_1, GROUP_6,
WELLORD1, TDGROUP, FINSEQ_4, NATTRA_1, FUNCT_6, MSUALG_4, MSUALG_5,
SETFAM_1, FUNCT_4, CANTOR_1, RELAT_2, MSUALG_9;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1,
RELAT_2, STRUCT_0, SETFAM_1, RELSET_1, FUNCT_1, EQREL_1, FUNCT_2,
FINSEQ_1, LANG1, MCART_1, FINSET_1, CARD_3, FINSEQ_4, CANTOR_1, TREES_4,
DTCONSTR, PBOOLE, MSUALG_1, MSUALG_2, PRALG_3, MSUALG_3, MSAFREE,
PRALG_2, PRE_CIRC, MSAFREE2, MSUALG_4, AUTALG_1, EXTENS_1, PZFMISC1,
MSSUBFAM, CLOSURE1, CLOSURE2, MSUALG_5;
constructors AUTALG_1, BINOP_1, CANTOR_1, CLOSURE1, CLOSURE2, EXTENS_1,
MSAFREE2, MSUALG_5, PRALG_3, PRE_CIRC, PZFMISC1, FINSEQ_4;
clusters CANTOR_1, CLOSURE2, EQREL_1, FINSET_1, MSAFREE, MSSUBFAM, MSUALG_1,
MSUALG_2, MSUALG_3, MSUALG_4, MSUALG_5, PRALG_1, PRALG_2, PRE_CIRC,
PZFMISC1, RELSET_1, STRUCT_0, ARYTM_3, XBOOLE_0, MEMBERED, PARTFUN1,
NUMBERS, ORDINAL2;
requirements SUBSET, BOOLE;
definitions AUTALG_1, FINSEQ_1, FUNCT_1, MSAFREE2, MSUALG_1, MSUALG_2,
MSUALG_3, MSUALG_4, PBOOLE, PRE_CIRC, TARSKI, XBOOLE_0;
theorems AUTALG_1, CANTOR_1, CARD_3, CLOSURE1, CLOSURE2, DTCONSTR, EXTENS_1,
EQREL_1, FINSEQ_1, FUNCOP_1, FUNCT_1, FUNCT_2, MCART_1, MSAFREE,
MSAFREE2, MSSUBFAM, MSUALG_1, MSUALG_2, MSUALG_3, MSUALG_4, MSUALG_5,
MSUALG_6, MSUALG_7, PARTFUN1, PBOOLE, PRALG_1, PRALG_2, PRALG_3,
PRE_CIRC, PZFMISC1, RELAT_2, SETFAM_1, TARSKI, RELSET_1, XBOOLE_0,
XBOOLE_1, ORDERS_1;
schemes MSSUBFAM, MSUALG_1, MSUALG_8, FUNCT_2;
begin :: Preliminaries
reserve a, I for set,
S for non empty non void ManySortedSign;
scheme MSSExD { I() -> non empty set, P[set,set] }:
ex f being ManySortedSet of I() st for i being Element of I() holds P[i,f.i]
provided
A1: for i being Element of I() ex j being set st P[i,j]
proof
defpred Z[set,set] means P[ $1,$2];
A2: for i being set st i in I() ex j being set st Z[i,j] by A1;
consider f being ManySortedSet of I() such that
A3: for i being set st i in I() holds Z[i,f.i] from MSSEx(A2);
take f;
let i be Element of I();
thus thesis by A3;
end;
definition let I be set,
M be ManySortedSet of I;
cluster locally-finite Element of Bool M;
existence
proof
[0]I c= M by PBOOLE:49;
then [0]I is ManySortedSubset of M by MSUALG_2:def 1;
then reconsider A = [0]I as Element of Bool M by CLOSURE2:def 1;
take A;
thus thesis;
end;
end;
definition let I be set,
M be non-empty ManySortedSet of I;
cluster non-empty locally-finite ManySortedSubset of M;
existence
proof
defpred P[set,set] means
ex a being Element of M.$1 st $2 = {a};
A1: now
let i be set such that i in I;
consider a being Element of M.i;
take j = {a};
thus P[i,j];
end;
consider C being ManySortedSet of I such that
A2: for i be set st i in I holds P[i,C.i] from MSSEx(A1);
C is ManySortedSubset of M
proof
let i be set; assume
A3: i in I;
then consider a being Element of M.i such that
A4: C.i = {a} by A2;
A5: M.i is non empty by A3,PBOOLE:def 16;
let q be set;
assume q in C.i;
then q = a by A4,TARSKI:def 1;
hence q in M.i by A5;
end;
then reconsider C as ManySortedSubset of M;
take C;
thus C is non-empty
proof
let i be set;
assume i in I;
then consider a being Element of M.i such that
A6: C.i = {a} by A2;
thus C.i is non empty by A6;
end;
let i be set;
assume i in I;
then consider a being Element of M.i such that
A7: C.i = {a} by A2;
thus C.i is finite by A7;
end;
end;
definition let S be non empty non void ManySortedSign,
A be non-empty MSAlgebra over S,
o be OperSymbol of S;
cluster -> FinSequence-like Element of Args(o,A);
coherence
proof
let x be Element of Args(o,A);
dom x = dom the_arity_of o by MSUALG_6:2;
then consider n being Nat such that
A1: dom x = Seg n by FINSEQ_1:def 2;
take n;
thus dom x = Seg n by A1;
end;
end;
definition let S be non void non empty ManySortedSign,
I be set,
s be SortSymbol of S,
F be MSAlgebra-Family of I, S;
cluster -> Function-like Relation-like Element of (SORTS F).s;
coherence
proof
let x be Element of (SORTS F).s;
x is Element of product Carrier(F,s) by PRALG_2:def 17;
hence x is Function-like Relation-like;
end;
end;
definition let S be non void non empty ManySortedSign,
X be non-empty ManySortedSet of the carrier of S;
cluster FreeGen X -> free non-empty;
coherence by MSAFREE:15,17;
end;
definition let S be non void non empty ManySortedSign,
X be non-empty ManySortedSet of the carrier of S;
cluster FreeMSA X -> free;
coherence by MSAFREE:18;
end;
definition let S be non empty non void ManySortedSign,
A, B be non-empty MSAlgebra over S;
cluster [:A,B:] -> non-empty;
coherence
proof
thus the Sorts of [:A,B:] is non-empty
proof
[:A,B:] = MSAlgebra (# [|the Sorts of A,the Sorts of B|],
[[:the Charact of A,the Charact of B:]] #) by PRALG_2:def 15;
hence thesis;
end;
end;
end;
theorem
for X, Y being set, f being Function st a in dom f & f.a in [:X,Y:]
holds f.a = [(pr1 f).a, (pr2 f).a]
proof
let X, Y be set,
f be Function such that
A1: a in dom f and
A2: f.a in [:X,Y:];
A3: (pr1 f).a = (f.a)`1 by A1,DTCONSTR:def 2;
(pr2 f).a = (f.a)`2 by A1,DTCONSTR:def 3;
hence thesis by A2,A3,MCART_1:23;
end;
theorem Th2:
for X being non empty set, Y being set, f being Function of X, {Y}
holds rng f = {Y}
proof
let X be non empty set,
Y be set,
f be Function of X, {Y};
A1: dom f = X by FUNCT_2:def 1;
thus rng f c= {Y} by RELSET_1:12;
let q be set;
assume q in {Y};
then A2: q = Y by TARSKI:def 1;
consider x being set such that
A3: x in X by XBOOLE_0:def 1;
f.x = Y by A3,FUNCT_2:65;
hence q in rng f by A1,A2,A3,FUNCT_1:def 5;
end;
theorem Th3:
for A being non empty finite set ex f being Function of NAT, A st rng f = A
proof
let A be non empty finite set;
consider p being FinSequence such that
A1: rng p = A by FINSEQ_1:73;
p is FinSequence of A
proof
thus rng p c= A by A1;
end;
then reconsider p as FinSequence of A;
defpred P[set,set] means
($1 in dom p implies $2 = p.$1) &
(not $1 in dom p implies ex a being Element of A st $2 = a);
A2: for x being Element of NAT ex y being Element of A st P[x,y]
proof
let x be Element of NAT;
per cases;
suppose x in dom p;
then reconsider px = p.x as Element of A by PARTFUN1:27;
take px;
thus x in dom p implies px = p.x;
thus thesis;
suppose
A3: not x in dom p;
consider a being Element of A;
take a;
thus x in dom p implies a = p.x by A3;
thus thesis;
end;
consider f being Function of NAT, A such that
A4: for x being Element of NAT holds P[x,f.x] from FuncExD(A2);
take f;
thus rng f c= A by RELSET_1:12;
let q be set;
assume q in A;
then consider x being Element of NAT such that
A5: x in dom p and
A6: q = p.x by A1,PARTFUN1:26;
A7: f.x = p.x by A4,A5;
dom f = NAT by FUNCT_2:def 1;
hence q in rng f by A6,A7,FUNCT_1:def 5;
end;
theorem Th4:
Class(nabla I) c= {I}
proof
let q be set;
assume q in Class(nabla I);
then consider x being set such that
A1: x in I & q = Class(nabla I,x) by EQREL_1:def 5;
Class(nabla I,x) = I by A1,EQREL_1:34;
hence q in {I} by A1,TARSKI:def 1;
end;
theorem Th5:
for I being non empty set holds Class(nabla I) = {I}
proof
let I be non empty set;
thus Class(nabla I) c= {I} by Th4;
let q be set;
assume q in {I};
then A1: q = I by TARSKI:def 1;
consider a being set such that
A2: a in I by XBOOLE_0:def 1;
Class(nabla I,a) = I by A2,EQREL_1:34;
hence q in Class(nabla I) by A1,A2,EQREL_1:def 5;
end;
theorem Th6:
ex A being ManySortedSet of I st {A} = I --> {a}
proof
deffunc F(set) = a;
consider A being ManySortedSet of I such that
A1: for i being set st i in I holds A.i = F(i) from MSSLambda;
take A;
now
let i be set; assume
A2: i in I;
hence {A}.i = {A.i} by PZFMISC1:def 1
.= {a} by A1,A2
.= (I --> {a}).i by A2,FUNCOP_1:13;
end;
hence thesis by PBOOLE:3;
end;
theorem
for A being ManySortedSet of I
ex B being non-empty ManySortedSet of I st A c= B
proof
let A be ManySortedSet of I;
consider a being set;
deffunc F(set) = {a} \/ A.$1;
consider f being ManySortedSet of I such that
A1: for i be set st i in I holds f.i = F(i) from MSSLambda;
f is non-empty
proof
let i be set;
assume i in I;
then f.i = {a} \/ A.i by A1;
hence f.i is non empty;
end;
then reconsider f as non-empty ManySortedSet of I;
take f;
let i be set;
assume i in I;
then f.i = A.i \/ {a} by A1;
hence A.i c= f.i by XBOOLE_1:7;
end;
theorem
for M being non-empty ManySortedSet of I
for B being locally-finite ManySortedSubset of M
ex C being non-empty locally-finite ManySortedSubset of M st B c= C
proof
let M be non-empty ManySortedSet of I,
B be locally-finite ManySortedSubset of M;
defpred P[set,set] means
ex a being Element of M.$1 st $2 = {a} \/ B.$1;
A1: now
let i be set such that i in I;
consider a being Element of M.i;
take j = {a} \/ B.i;
thus P[i,j];
end;
consider C being ManySortedSet of I such that
A2: for i be set st i in I holds P[i,C.i] from MSSEx(A1);
A3: C is ManySortedSubset of M
proof
let i be set; assume
A4: i in I;
then consider a being Element of M.i such that
A5: C.i = {a} \/ B.i by A2;
B c= M by MSUALG_2:def 1;
then A6: B.i c= M.i by A4,PBOOLE:def 5;
A7: M.i is non empty by A4,PBOOLE:def 16;
let q be set;
assume q in C.i;
then q in {a} or q in B.i by A5,XBOOLE_0:def 2;
then q = a or q in M.i by A6,TARSKI:def 1;
hence q in M.i by A7;
end;
A8: C is non-empty
proof
let i be set;
assume i in I;
then consider a being Element of M.i such that
A9: C.i = {a} \/ B.i by A2;
thus C.i is non empty by A9;
end;
C is locally-finite
proof
let i be set; assume
A10: i in I;
then consider a being Element of M.i such that
A11: C.i = {a} \/ B.i by A2;
reconsider b = B.i as finite set by A10,PRE_CIRC:def 3;
{a} \/ b is finite;
hence C.i is finite by A11;
end;
then reconsider C as non-empty locally-finite ManySortedSubset of M
by A3,A8;
take C;
let i be set;
assume i in I;
then consider a being Element of M.i such that
A12: C.i = {a} \/ B.i by A2;
thus B.i c= C.i by A12,XBOOLE_1:7;
end;
theorem
for A, B being ManySortedSet of I
for F, G being ManySortedFunction of A, {B} holds F = G
proof
let A, B be ManySortedSet of I,
F, G be ManySortedFunction of A, {B};
now
let i be set; assume
A1: i in I;
then A2: F.i is Function of A.i, {B}.i & G.i is Function of A.i, {B}.
i
by MSUALG_1:def 2;
{B}.i = {B.i} by A1,PZFMISC1:def 1;
hence F.i = G.i by A2,FUNCT_2:66;
end;
hence F = G by PBOOLE:3;
end;
theorem Th10:
for A being non-empty ManySortedSet of I, B being ManySortedSet of I
for F being ManySortedFunction of A, {B} holds F is "onto"
proof
let A be non-empty ManySortedSet of I,
B be ManySortedSet of I,
F be ManySortedFunction of A, {B};
let i be set; assume
A1: i in I;
then A2: A.i <> {} by PBOOLE:def 16;
A3: {B}.i = {B.i} by A1,PZFMISC1:def 1;
F.i is Function of A.i, {B}.i by A1,MSUALG_1:def 2;
hence rng(F.i) = {B}.i by A2,A3,Th2;
end;
theorem Th11:
for A being ManySortedSet of I, B being non-empty ManySortedSet of I
for F being ManySortedFunction of {A}, B holds F is "1-1"
proof
let A be ManySortedSet of I,
B be non-empty ManySortedSet of I,
F be ManySortedFunction of {A}, B;
now
let i be set; assume
A1: i in I;
then A2: {A}.i = {A.i} by PZFMISC1:def 1;
F.i is Function of {A}.i, B.i by A1,MSUALG_1:def 2;
hence F.i is one-to-one by A2,PARTFUN1:70;
end;
hence F is "1-1" by MSUALG_3:1;
end;
theorem
for X being non-empty ManySortedSet of the carrier of S
holds Reverse X is "1-1"
proof
let X be non-empty ManySortedSet of the carrier of S;
for i being set st i in the carrier of S
holds (Reverse X).i is one-to-one
proof
let i be set;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
set f = (Reverse X).s;
let x1,x2 be set such that
A1: x1 in dom ((Reverse X).i) and
A2: x2 in dom ((Reverse X).i) and
A3: ((Reverse X).i).x1 = ((Reverse X).i).x2;
A4: f = Reverse(s,X) by MSAFREE:def 20;
then A5: dom f = FreeGen(s,X) by FUNCT_2:def 1;
then consider a1 being set such that
A6: a1 in X.s and
A7: x1 = root-tree [a1,s] by A1,MSAFREE:def 17;
consider a2 being set such that
A8: a2 in X.s and
A9: x2 = root-tree [a2,s] by A2,A5,MSAFREE:def 17;
set D = DTConMSA X;
A10: [a1,s] in Terminals D by A6,MSAFREE:7;
then reconsider t1 = [a1,s] as Symbol of D;
t1`2 = s by MCART_1:7;
then root-tree t1 in {root-tree tt where tt is Symbol of D :
tt in Terminals D & tt`2 = s} by A10;
then root-tree t1 in FreeGen(s,X) by MSAFREE:14;
then A11: f.x1 = [a1,s]`1 by A4,A7,MSAFREE:def 19
.= a1 by MCART_1:7;
A12: [a2,s] in Terminals D by A8,MSAFREE:7;
then reconsider t2 = [a2,s] as Symbol of D;
t2`2 = s by MCART_1:7;
then root-tree t2 in {root-tree tt where tt is Symbol of D :
tt in Terminals D & tt`2 = s} by A12;
then root-tree t2 in FreeGen(s,X) by MSAFREE:14;
then f.x2 = [a2,s]`1 by A4,A9,MSAFREE:def 19
.= a2 by MCART_1:7;
hence x1 = x2 by A3,A7,A9,A11;
end;
hence Reverse X is "1-1" by MSUALG_3:1;
end;
theorem
for A being non-empty locally-finite ManySortedSet of I
ex F being ManySortedFunction of I --> NAT, A st F is "onto"
proof
let A be non-empty locally-finite ManySortedSet of I;
defpred P[set,set] means
ex f being Function of NAT, A.$1 st $2 = f & rng f = A.$1;
A1: for i being set st i in I ex j being set st P[i,j]
proof
let i be set;
assume i in I;
then A.i is non empty & A.i is finite by PBOOLE:def 16,PRE_CIRC:def 3;
then consider f being Function of NAT, A.i such that
A2: rng f = A.i by Th3;
take j = f;
thus P[i,j] by A2;
end;
consider F being ManySortedSet of I such that
A3: for i being set st i in I holds P[i,F.i] from MSSEx(A1);
F is ManySortedFunction of I --> NAT, A
proof
let i be set; assume
A4: i in I;
then consider f being Function of NAT, A.i such that
A5: F.i = f and rng f = A.i by A3;
(I --> NAT).i = NAT by A4,FUNCOP_1:13;
hence F.i is Function of (I --> NAT).i, A.i by A5;
end;
then reconsider F as ManySortedFunction of I --> NAT, A;
take F;
let i be set;
assume i in I;
then consider f being Function of NAT, A.i such that
A6: F.i = f & rng f = A.i by A3;
thus rng (F.i) = A.i by A6;
end;
theorem
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for f, g being Element of product the Sorts of A st
for i being set holds proj(the Sorts of A,i).f = proj(the Sorts of A,i).g
holds f = g
proof
let S be non empty ManySortedSign,
A be non-empty MSAlgebra over S,
f, g be Element of product the Sorts of A such that
A1: for i being set holds proj(the Sorts of A,i).f =
proj(the Sorts of A,i).g;
set X = the Sorts of A;
now
thus dom f = dom X by CARD_3:18
.= dom g by CARD_3:18;
let x be set such that x in dom f;
A2: dom (proj(X,x)) = product X by PRALG_3:def 2;
hence f.x = proj(X,x).f by PRALG_3:def 2
.= proj(X,x).g by A1
.= g.x by A2,PRALG_3:def 2;
end;
hence f = g by FUNCT_1:9;
end;
theorem
for I being non empty set
for s being Element of S
for A being MSAlgebra-Family of I,S
for f, g being Element of product Carrier(A,s) st
for a being Element of I
holds proj(Carrier(A,s),a).f = proj(Carrier(A,s),a).g
holds f = g
proof
let I be non empty set,
s be Element of S,
A be MSAlgebra-Family of I,S,
f, g be Element of product Carrier(A,s) such that
A1: for a being Element of I
holds proj(Carrier(A,s),a).f = proj(Carrier(A,s),a).g;
now
A2: dom f = dom Carrier(A,s) by CARD_3:18;
hence dom f = dom g by CARD_3:18;
let x be set such that
A3: x in dom f;
A4: dom f = I by A2,PBOOLE:def 3;
A5: dom (proj(Carrier(A,s),x)) = product Carrier(A,s) by PRALG_3:def 2;
hence f.x = proj(Carrier(A,s),x).f by PRALG_3:def 2
.= proj(Carrier(A,s),x).g by A1,A3,A4
.= g.x by A5,PRALG_3:def 2;
end;
hence f = g by FUNCT_1:9;
end;
theorem
for A, B being non-empty MSAlgebra over S
for C being non-empty MSSubAlgebra of A
for h1 being ManySortedFunction of B, C st h1 is_homomorphism B, C
for h2 being ManySortedFunction of B, A st h1 = h2
holds h2 is_homomorphism B, A
proof
let A, B be non-empty MSAlgebra over S,
C be non-empty MSSubAlgebra of A,
h1 be ManySortedFunction of B, C such that
A1: h1 is_homomorphism B, C;
let h2 be ManySortedFunction of B, A such that
A2: h1 = h2;
the Sorts of C is ManySortedSubset of the Sorts of A
by MSUALG_2:def 10;
then id (the Sorts of C) is ManySortedFunction of C, A
by EXTENS_1:9;
then consider G be ManySortedFunction of C, A such that
A3: G = id (the Sorts of C);
A4: G ** h1 = h1 by A3,MSUALG_3:4;
G is_monomorphism C, A by A3,MSUALG_3:22;
then G is_homomorphism C, A by MSUALG_3:def 11;
hence h2 is_homomorphism B, A by A1,A2,A4,MSUALG_3:10;
end;
theorem
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A, B st F is_monomorphism A, B
holds A, Image F are_isomorphic
proof
let A, B be non-empty MSAlgebra over S,
F be ManySortedFunction of A, B; assume
A1: F is_monomorphism A, B;
then F is_homomorphism A, B by MSUALG_3:def 11;
then consider G being ManySortedFunction of A, Image F such that
A2: G = F and
A3: G is_epimorphism A, Image F by MSUALG_3:21;
take G;
thus G is_epimorphism A, Image F by A3;
thus G is_homomorphism A, Image F by A3,MSUALG_3:def 10;
thus G is "1-1" by A1,A2,MSUALG_3:def 11;
end;
theorem Th18:
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A, B st F is "onto"
for o being OperSymbol of S
for x being Element of Args(o,B) holds
ex y being Element of Args(o,A) st F # y = x
proof
let A, B be non-empty MSAlgebra over S,
F be ManySortedFunction of A, B such that
A1: F is "onto";
let o be OperSymbol of S,
t be Element of Args(o,B);
set D = len (the_arity_of o);
reconsider E = (the Sorts of B)*(the_arity_of o)
as non-empty ManySortedSet of dom (the_arity_of o);
A2: Args(o,B) = product E by PRALG_2:10;
A3: Seg D = dom the_arity_of o by FINSEQ_1:def 3
.= dom ((the Sorts of B)*(the_arity_of o)) by PRALG_2:10
.= dom t by A2,CARD_3:18;
defpred P[set,set] means
ex y1 being Element of (the Sorts of A).((the_arity_of o)/.$1)
st (F.((the_arity_of o)/.$1)).y1 = t.$1 & $2 = y1;
A4: for k being Nat st k in Seg D ex x being set st P[k,x]
proof
let k be Nat such that
A5: k in Seg D;
set s = (the_arity_of o)/.k;
A6: rng (F.s) = (the Sorts of B).s by A1,MSUALG_3:def 3;
k in dom the_arity_of o by A5,FINSEQ_1:def 3;
then t.k in (the Sorts of B).s by MSUALG_6:2;
then consider y1 being set such that
A7: y1 in (the Sorts of A).s & F.s.y1 = t.k by A6,FUNCT_2:17;
take y1;
reconsider y2 = y1 as Element of (the Sorts of A).s by A7;
take y2;
thus thesis by A7;
end;
consider p being FinSequence such that
A8: dom p = Seg D and
A9: for k being Nat st k in Seg D holds P[k,p.k] from NonUniqSeqEx(A4);
A10: len p = len the_arity_of o by A8,FINSEQ_1:def 3;
for k being Nat st k in dom p holds
p.k in (the Sorts of A).((the_arity_of o)/.k)
proof
let k be Nat;
assume k in dom p;
then consider y1 being Element of (the Sorts of A).((the_arity_of o)/.k)
such that
F.((the_arity_of o)/.k).y1 = t.k and
A11: p.k = y1 by A8,A9;
thus p.k in (the Sorts of A).((the_arity_of o)/.k) by A11;
end;
then reconsider p as Element of Args(o,A) by A10,MSAFREE2:7;
set fp = F # p;
take p;
A12: dom fp = dom ((the Sorts of B)*(the_arity_of o)) by A2,CARD_3:18
.= dom t by A2,CARD_3:18;
for k being Nat st k in dom t holds fp.k = t.k
proof
let k be Nat; assume
A13: k in dom t;
then consider y1 being Element of (the Sorts of A).((the_arity_of o)/.k)
such that
A14: (F.((the_arity_of o)/.k)).y1 = t.k & p.k = y1 by A3,A9;
thus fp.k = t.k by A3,A8,A13,A14,MSUALG_3:def 8;
end;
hence F # p = t by A12,FINSEQ_1:17;
end;
theorem Th19:
for A being non-empty MSAlgebra over S, o being OperSymbol of S
for x being Element of Args(o,A) holds
Den(o,A).x in (the Sorts of A).(the_result_sort_of o)
proof
let A be non-empty MSAlgebra over S,
o be OperSymbol of S,
x be Element of Args(o,A);
Den(o,A).x is Element of ((the Sorts of A) * the ResultSort of S).o
by MSUALG_1:def 10;
then Den(o,A).x is Element of (the Sorts of A).((the ResultSort of S).o)
by FUNCT_2:21;
then Den(o,A).x is Element of (the Sorts of A).(the_result_sort_of o)
by MSUALG_1:def 7;
hence thesis;
end;
theorem Th20:
for A, B, C being non-empty MSAlgebra over S
for F1 being ManySortedFunction of A, B
for F2 being ManySortedFunction of A, C st
F1 is_epimorphism A, B & F2 is_homomorphism A, C
for G being ManySortedFunction of B, C st G ** F1 = F2
holds G is_homomorphism B, C
proof
let A, B, C be non-empty MSAlgebra over S,
F1 be ManySortedFunction of A, B,
F2 be ManySortedFunction of A, C such that
A1: F1 is_epimorphism A, B and
A2: F2 is_homomorphism A, C;
let G be ManySortedFunction of B, C such that
A3: G ** F1 = F2;
let o be OperSymbol of S such that Args(o,B) <> {};
let x be Element of Args(o,B);
set r = the_result_sort_of o;
F1 is "onto" by A1,MSUALG_3:def 10;
then consider y being Element of Args(o,A) such that
A4: F1 # y = x by Th18;
F1 is_homomorphism A, B by A1,MSUALG_3:def 10;
then A5: (F1.r).(Den(o,A).y) = Den(o,B).x by A4,MSUALG_3:def 9;
A6: Den(o,A).y is Element of (the Sorts of A).r by Th19;
A7: (F2.r).(Den(o,A).y) = Den(o,C).((G ** F1) # y) by A2,A3,MSUALG_3:def 9
.= Den(o,C).(G # x) by A4,MSUALG_3:8;
(F2.r).(Den(o,A).y) = (G.r * F1.r).(Den(o,A).y) by A3,MSUALG_3:2
.= (G.r).(Den(o,B).x) by A5,A6,FUNCT_2:21;
hence (G.(the_result_sort_of o)).(Den(o,B).x) = Den(o,C).(G#x) by A7;
end;
reserve A, M for ManySortedSet of I,
B, C for non-empty ManySortedSet of I;
definition let I be set;
let A be ManySortedSet of I;
let B, C be non-empty 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
proof
deffunc G(set) = pr1 (F.$1);
consider X be ManySortedSet of I such that
A1: for i be set st i in I holds X.i = G(i) from MSSLambda;
X is ManySortedFunction of A, B
proof
let i be set; assume
A2: i in I;
then A3: [|B,C|].i <> {} by PBOOLE:def 16;
A4: X.i = pr1 (F.i) by A1,A2;
reconsider Bi = B.i as non empty set by A2,PBOOLE:def 16;
reconsider Xi = X.i as Function by A4;
A5: F.i is Function of A.i, [|B,C|].i by A2,MSUALG_1:def 2;
then dom (F.i) = A.i by A3,FUNCT_2:def 1;
then A6: dom Xi = A.i by A4,DTCONSTR:def 2;
rng Xi c= Bi
proof
let q be set such that
A7: q in rng Xi;
assume
A8: not q in Bi;
consider x be set such that
A9: x in dom Xi and
A10: Xi.x = q by A7,FUNCT_1:def 5;
A11: x in dom (F.i) by A4,A9,DTCONSTR:def 2;
then A12: Xi.x = (F.i.x)`1 by A4,DTCONSTR:def 2;
rng (F.i) c= [|B,C|].i by A5,RELSET_1:12;
then A13: rng (F.i) c= [:B.i,C.i:] by A2,PRALG_2:def 9;
F.i.x in rng (F.i) by A11,FUNCT_1:def 5;
hence contradiction by A8,A10,A12,A13,MCART_1:10;
end;
hence X.i is Function of A.i, B.i by A6,FUNCT_2:def 1,RELSET_1:11;
end;
then reconsider X as ManySortedFunction of A, B;
take X;
thus thesis by A1;
end;
uniqueness
proof
let M, N be ManySortedFunction of A, B such that
A14: (for i be set st i in I holds M.i = pr1 (F.i)) and
A15: (for i be set st i in I holds N.i = pr1 (F.i));
now
let i be set; assume
A16: i in I;
hence M.i = pr1 (F.i) by A14
.= N.i by A15,A16;
end;
hence M = N by PBOOLE:3;
end;
func Mpr2 F -> ManySortedFunction of A, C means :Def2:
for i being set st i in I holds it.i = pr2 (F.i);
existence
proof
deffunc G(set) =pr2 (F.$1);
consider X be ManySortedSet of I such that
A17: for i be set st i in I holds X.i = G(i) from MSSLambda;
X is ManySortedFunction of A, C
proof
let i be set; assume
A18: i in I;
then A19: [|B,C|].i <> {} by PBOOLE:def 16;
A20: X.i = pr2 (F.i) by A17,A18;
reconsider Ci = C.i as non empty set by A18,PBOOLE:def 16;
reconsider Xi = X.i as Function by A20;
A21: F.i is Function of A.i, [|B,C|].i by A18,MSUALG_1:def 2;
then dom (F.i) = A.i by A19,FUNCT_2:def 1;
then A22: dom Xi = A.i by A20,DTCONSTR:def 3;
rng Xi c= Ci
proof
let q be set such that
A23: q in rng Xi;
assume
A24: not q in Ci;
consider x be set such that
A25: x in dom Xi and
A26: Xi.x = q by A23,FUNCT_1:def 5;
A27: x in dom (F.i) by A20,A25,DTCONSTR:def 3;
then A28: Xi.x = (F.i.x)`2 by A20,DTCONSTR:def 3;
rng (F.i) c= [|B,C|].i by A21,RELSET_1:12;
then A29: rng (F.i) c= [:B.i,C.i:] by A18,PRALG_2:def 9;
F.i.x in rng (F.i) by A27,FUNCT_1:def 5;
hence contradiction by A24,A26,A28,A29,MCART_1:10;
end;
hence X.i is Function of A.i, C.i by A22,FUNCT_2:def 1,RELSET_1:11;
end;
then reconsider X as ManySortedFunction of A, C;
take X;
thus thesis by A17;
end;
uniqueness
proof
let M, N be ManySortedFunction of A, C such that
A30: (for i be set st i in I holds M.i = pr2 (F.i)) and
A31: (for i be set st i in I holds N.i = pr2 (F.i));
now
let i be set; assume
A32: i in I;
hence M.i = pr2 (F.i) by A30
.= N.i by A31,A32;
end;
hence M = N by PBOOLE:3;
end;
end;
theorem
for F being ManySortedFunction of A, [| I-->{a} , I-->{a} |]
holds Mpr1 F = Mpr2 F
proof
let F be ManySortedFunction of A, [| I-->{a} , I-->{a} |];
now
let i be set; assume
A1: i in I;
then A2: (Mpr1 F).i = pr1 (F.i) by Def1;
A3: (Mpr2 F).i = pr2 (F.i) by A1,Def2;
A4: dom (pr2 (F.i)) = dom (F.i) by DTCONSTR:def 3;
now
let y be set such that
A5: y in dom (F.i);
A6: (F.i) is Function of A.i, [| I-->{a} , I-->{a} |].i
by A1,MSUALG_1:def 2;
A7: (F.i).y in rng (F.i) by A5,FUNCT_1:def 5;
rng (F.i) c= [| I-->{a} , I-->{a} |].i by A6,RELSET_1:12;
then A8: rng (F.i) c= [: (I-->{a}).i , (I-->{a}).i :] by A1,PRALG_2:def 9;
then ((F.i).y)`1 in (I-->{a}).i by A7,MCART_1:10;
then A9: ((F.i).y)`1 in {a} by A1,FUNCOP_1:13;
((F.i).y)`2 in (I-->{a}).i by A7,A8,MCART_1:10;
then A10: ((F.i).y)`2 in {a} by A1,FUNCOP_1:13;
thus (pr2 (F.i)).y = ((F.i).y)`2 by A5,DTCONSTR:def 3
.= a by A10,TARSKI:def 1
.= ((F.i).y)`1 by A9,TARSKI:def 1;
end;
hence (Mpr1 F).i = (Mpr2 F).i by A2,A3,A4,DTCONSTR:def 2;
end;
hence Mpr1 F = Mpr2 F by PBOOLE:3;
end;
theorem
for F being ManySortedFunction of A, [|B,C|] st F is "onto"
holds Mpr1 F is "onto"
proof
let F be ManySortedFunction of A, [|B,C|] such that
A1: F is "onto";
let i be set; assume
A2: i in I;
then reconsider m = (Mpr1 F).i as Function of A.i, B.i by MSUALG_1:def 2;
rng m = B.i
proof
A is_transformable_to B
proof
let j be set;
assume j in I;
hence B.j = {} implies A.j = {} by PBOOLE:def 16;
end;
then rngs Mpr1 F c= B by MSSUBFAM:17;
then (rngs Mpr1 F).i c= B.i by A2,PBOOLE:def 5;
hence rng m c= B.i by A2,MSSUBFAM:13;
let a be set such that
A3: a in B.i;
A4: (F.i) is Function of A.i, [|B,C|].i by A2,MSUALG_1:def 2;
A5: rng (F.i) = [|B,C|].i by A1,A2,MSUALG_3:def 3;
A6: [|B,C|].i <> {} by A2,PBOOLE:def 16;
then consider z be set such that
A7: z in [|B,C|].i by XBOOLE_0:def 1;
A8: z in [:B.i,C.i:] by A2,A7,PRALG_2:def 9;
set p = [a,z`2];
A9: p`1 in B.i by A3,MCART_1:7;
p`2 = z`2 by MCART_1:7;
then p`2 in C.i by A8,MCART_1:10;
then p in [:B.i,C.i:] by A9,MCART_1:11;
then p in [|B,C|].i by A2,PRALG_2:def 9;
then consider b be set such that
A10: b in A.i and
A11: (F.i).b = p by A4,A5,FUNCT_2:17;
A12: dom (F.i) = A.i by A4,A6,FUNCT_2:def 1;
B.i <> {} by A2,PBOOLE:def 16;
then A13: dom m = A.i by FUNCT_2:def 1;
m.b = (pr1 (F.i)).b by A2,Def1
.= p`1 by A10,A11,A12,DTCONSTR:def 2
.= a by MCART_1:7;
hence a in rng m by A10,A13,FUNCT_1:def 5;
end;
hence thesis;
end;
theorem
for F being ManySortedFunction of A, [|B,C|] st F is "onto"
holds Mpr2 F is "onto"
proof
let F be ManySortedFunction of A, [|B,C|] such that
A1: F is "onto";
let i be set; assume
A2: i in I;
then reconsider m = (Mpr2 F).i as Function of A.i, C.i by MSUALG_1:def 2;
rng m = C.i
proof
A is_transformable_to C
proof
let j be set;
assume j in I;
hence C.j = {} implies A.j = {} by PBOOLE:def 16;
end;
then rngs Mpr2 F c= C by MSSUBFAM:17;
then (rngs Mpr2 F).i c= C.i by A2,PBOOLE:def 5;
hence rng m c= C.i by A2,MSSUBFAM:13;
let a be set such that
A3: a in C.i;
A4: (F.i) is Function of A.i, [|B,C|].i by A2,MSUALG_1:def 2;
A5: rng (F.i) = [|B,C|].i by A1,A2,MSUALG_3:def 3;
A6: [|B,C|].i <> {} by A2,PBOOLE:def 16;
then consider z be set such that
A7: z in [|B,C|].i by XBOOLE_0:def 1;
A8: z in [:B.i,C.i:] by A2,A7,PRALG_2:def 9;
set p = [z`1,a];
A9: p`2 in C.i by A3,MCART_1:7;
p`1 = z`1 by MCART_1:7;
then p`1 in B.i by A8,MCART_1:10;
then p in [:B.i,C.i:] by A9,MCART_1:11;
then p in [|B,C|].i by A2,PRALG_2:def 9;
then consider b be set such that
A10: b in A.i and
A11: (F.i).b = p by A4,A5,FUNCT_2:17;
A12: dom (F.i) = A.i by A4,A6,FUNCT_2:def 1;
C.i <> {} by A2,PBOOLE:def 16;
then A13: dom m = A.i by FUNCT_2:def 1;
m.b = (pr2 (F.i)).b by A2,Def2
.= p`2 by A10,A11,A12,DTCONSTR:def 3
.= a by MCART_1:7;
hence a in rng m by A10,A13,FUNCT_1:def 5;
end;
hence thesis;
end;
theorem
for F being ManySortedFunction of A, [|B,C|] st M in doms F holds
for i be set st i in I holds (F..M).i = [((Mpr1 F)..M).i, ((Mpr2 F)..M).i]
proof
let F be ManySortedFunction of A, [|B,C|] such that
A1: M in doms F;
let i be set; assume
A2: i in I;
then A3: (Mpr1 F).i = pr1 (F.i) by Def1;
A4: (Mpr2 F).i = pr2 (F.i) by A2,Def2;
A5: dom F = I by PBOOLE:def 3;
A is_transformable_to [|B,C|]
proof
let i be set;
assume i in I;
hence [|B,C|].i = {} implies A.i = {} by PBOOLE:def 16;
end;
then M in A by A1,MSSUBFAM:17;
then F..M in [|B,C|] by CLOSURE1:3;
then (F..M).i in [|B,C|].i by A2,PBOOLE:def 4;
then (F..M).i in [:B.i,C.i:] by A2,PRALG_2:def 9;
then A6: (F.i).(M.i) in [:B.i,C.i:] by A2,A5,PRALG_1:def 18;
set z = (F.i).(M.i);
M.i in (doms F).i by A1,A2,PBOOLE:def 4;
then A7: M.i in dom (F.i) by A2,MSSUBFAM:14;
dom (Mpr1 F) = I by PBOOLE:def 3;
then A8: ((Mpr1 F)..M).i = (pr1 (F.i)).(M.i) by A2,A3,PRALG_1:def 18
.= z`1 by A7,DTCONSTR:def 2;
dom (Mpr2 F) = I by PBOOLE:def 3;
then ((Mpr2 F)..M).i = (pr2 (F.i)).(M.i) by A2,A4,PRALG_1:def 18
.= z`2 by A7,DTCONSTR:def 3;
then z = [((Mpr1 F)..M).i, ((Mpr2 F)..M).i] by A6,A8,MCART_1:23;
hence thesis by A2,A5,PRALG_1:def 18;
end;
begin :: On the Trivial Many Sorted Algebras
definition let S be non empty ManySortedSign;
cluster the Sorts of Trivial_Algebra S -> locally-finite non-empty;
coherence
proof
consider A being ManySortedSet of the carrier of S such that
A1: {A} = (the carrier of S) --> {0} by Th6;
thus thesis by A1,MSAFREE2:def 12;
end;
end;
definition let S be non empty ManySortedSign;
cluster Trivial_Algebra S -> locally-finite non-empty;
coherence
proof
thus the Sorts of Trivial_Algebra S is locally-finite;
let i be set such that
A1: i in the carrier of S;
the Sorts of Trivial_Algebra S = (the carrier of S) --> {0}
by MSAFREE2:def 12;
hence (the Sorts of Trivial_Algebra S).i is non empty by A1,FUNCOP_1:13;
end;
end;
theorem Th25:
for A being non-empty MSAlgebra over S
for F being ManySortedFunction of A, Trivial_Algebra S
for o being OperSymbol of S
for x being Element of Args(o,A) holds
(F.the_result_sort_of o).(Den(o,A).x) = 0 &
Den(o,Trivial_Algebra S).(F#x) = 0
proof
let A be non-empty MSAlgebra over S,
F be ManySortedFunction of A, Trivial_Algebra S;
let o be OperSymbol of S;
let x be Element of Args(o,A);
set I = the carrier of S,
SA = the Sorts of A,
T = Trivial_Algebra S,
ST = the Sorts of T;
consider XX being ManySortedSet of I such that
A1: {XX} = I --> {0} by Th6;
A2: ST = {XX} by A1,MSAFREE2:def 12;
set r = the_result_sort_of o;
consider i being set such that
A3: i in I and
A4: Result(o,T) = ST.i by MSUALG_1:2;
A5: ST.i = {0} by A1,A2,A3,FUNCOP_1:13;
Den(o,A).x in Result(o,A);
then Den(o,A).x in ((the Sorts of A) * the ResultSort of S).o
by MSUALG_1:def 10;
then Den(o,A).x in (the Sorts of A).((the ResultSort of S).o)
by FUNCT_2:21;
then reconsider d = Den(o,A).x as Element of SA.r by MSUALG_1:def 7;
A6: ST.r = {0} by A1,A2,FUNCOP_1:13;
thus (F.r).(Den(o,A).x) = (F.r).d
.= 0 by A6,TARSKI:def 1;
thus Den(o,T).(F#x) = 0 by A4,A5,TARSKI:def 1;
end;
theorem Th26:
for A being non-empty MSAlgebra over S
for F being ManySortedFunction of A, Trivial_Algebra S holds
F is_epimorphism A, Trivial_Algebra S
proof
let A be non-empty MSAlgebra over S,
F be ManySortedFunction of A, Trivial_Algebra S;
set I = the carrier of S;
consider XX being ManySortedSet of I such that
A1: {XX} = I --> {0} by Th6;
A2: the Sorts of Trivial_Algebra S = {XX} by A1,MSAFREE2:def 12;
thus F is_homomorphism A, Trivial_Algebra S
proof
let o be OperSymbol of S such that Args(o,A) <> {};
let x be Element of Args(o,A);
thus (F.the_result_sort_of o).(Den(o,A).x) = 0 by Th25
.= Den(o,Trivial_Algebra S).(F#x) by Th25;
end;
thus F is "onto" by A2,Th10;
end;
theorem
for A being MSAlgebra over S st
ex X being ManySortedSet of the carrier of S st the Sorts of A = {X}
holds A, Trivial_Algebra S are_isomorphic
proof
let A be MSAlgebra over S such that
A1: ex X being ManySortedSet of the carrier of S st the Sorts of A = {X};
set I = the carrier of S,
SB = the Sorts of A,
ST = the Sorts of Trivial_Algebra S;
consider X being ManySortedSet of I such that
A2: the Sorts of A = {X} by A1;
consider F being ManySortedFunction of SB, ST;
take F;
reconsider F1 = F as ManySortedFunction of {X}, ST by A2;
A is non-empty by A2,MSUALG_1:def 8;
hence F is_epimorphism A, Trivial_Algebra S by Th26;
hence F is_homomorphism A, Trivial_Algebra S by MSUALG_3:def 10;
F1 is "1-1" by Th11;
hence F is "1-1";
end;
begin :: On the Many Sorted Congruences
theorem
for A being non-empty MSAlgebra over S
for C being MSCongruence of A holds
C is ManySortedSubset of [|the Sorts of A, the Sorts of A|]
proof
let A be non-empty MSAlgebra over S,
C be MSCongruence of A;
let i be set such that
A1: i in the carrier of S;
set SF = the Sorts of A;
C.i is Relation of SF.i, SF.i by A1,MSUALG_4:def 2;
then C.i c= [:SF.i, SF.i:];
hence C.i c= [|SF,SF|].i by A1,PRALG_2:def 9;
end;
theorem
for A being non-empty MSAlgebra over S
for R being Subset of CongrLatt A
for F being SubsetFamily of [|the Sorts of A, the Sorts of A|]
st R = F holds meet |:F:| is MSCongruence of A
proof
let A be non-empty MSAlgebra over S,
R be Subset of CongrLatt A,
F be SubsetFamily of [|the Sorts of A, the Sorts of A|]
such that
A1: R = F;
set R0 = meet |:F:|,
SF = the Sorts of A,
I = the carrier of S;
per cases;
suppose F is non empty;
then reconsider F1 = F as non empty SubsetFamily of [|SF,SF|];
F1 c= the carrier of EqRelLatt SF
proof
let q be set;
assume q in F1;
then q is MSCongruence of A by A1,MSUALG_5:def 6;
hence q in the carrier of EqRelLatt SF by MSUALG_5:def 5;
end;
then A2: R0 is MSEquivalence_Relation-like ManySortedRelation of SF
by MSUALG_7:9;
then reconsider R0 as ManySortedRelation of A;
R0 is MSEquivalence-like
proof
let i be set,
R be Relation of SF.i;
assume i in I & R0.i = R;
hence R is Equivalence_Relation of SF.i by A2,MSUALG_4:def 3;
end;
then reconsider R0 as MSEquivalence-like ManySortedRelation of A;
now
let o be OperSymbol of S;
let a,b be Element of Args(o,A) such that
A3: for n being Nat st n in dom a holds [a.n,b.n] in
R0.((the_arity_of o)/.n);
set r = the_result_sort_of o;
consider Q being Subset-Family of ([|SF,SF|].r) such that
A4: Q = |:F1:|.r and
A5: R0.r = Intersect Q by MSSUBFAM:def 2;
A6: Q = { s.r where s is Element of Bool [|SF,SF|] : s in F1 }
by A4,CLOSURE2:15;
now
let Y be set;
assume Y in Q;
then consider s being Element of Bool [|SF,SF|] such that
A7: Y = s.r and
A8: s in F1 by A6;
reconsider s as MSCongruence of A by A1,A8,MSUALG_5:def 6;
now
let n be Nat such that
A9: n in dom a;
set t = (the_arity_of o)/.n;
consider G being Subset-Family of ([|SF,SF|].t) such that
A10: G = |:F1:|.t and
A11: R0.t = Intersect G by MSSUBFAM:def 2;
[a.n,b.n] in Intersect G by A3,A9,A11;
then A12: [a.n,b.n] in meet G by A10,CANTOR_1:def 3;
G = { j.t where j is Element of Bool [|SF,SF|] : j in F1 }
by A10,CLOSURE2:15;
then s.t in G by A8;
hence [a.n,b.n] in s.t by A12,SETFAM_1:def 1;
end;
hence [Den(o,A).a,Den(o,A).b] in Y by A7,MSUALG_4:def 6;
end;
then [Den(o,A).a,Den(o,A).b] in meet Q by A4,SETFAM_1:def 1;
hence [Den(o,A).a,Den(o,A).b] in R0.(the_result_sort_of o)
by A4,A5,CANTOR_1:def 3;
end;
hence thesis by MSUALG_4:def 6;
suppose F is empty;
then |:F:| = [0]I by CLOSURE2:def 4;
then meet |:F:| = [|the Sorts of A, the Sorts of A|] by MSSUBFAM:41;
hence thesis by MSUALG_5:20;
end;
theorem
for A being non-empty MSAlgebra over S
for C being MSCongruence of A st C = [|the Sorts of A, the Sorts of A|]
holds the Sorts of QuotMSAlg (A,C) = {the Sorts of A}
proof
let A be non-empty MSAlgebra over S,
C be MSCongruence of A such that
A1: C = [|the Sorts of A, the Sorts of A|];
now
let i be set;
assume i in the carrier of S;
then reconsider s = i as Element of S;
A2: QuotMSAlg (A,C) = MSAlgebra (# Class C, QuotCharact C #)
by MSUALG_4:def 16;
A3: C.s = [:(the Sorts of A).s, (the Sorts of A).s:] by A1,PRALG_2:def 9
.= nabla (the Sorts of A).s by EQREL_1:def 1;
thus (the Sorts of QuotMSAlg (A,C)).i
= Class (C.s) by A2,MSUALG_4:def 8
.= {(the Sorts of A).s} by A3,Th5
.= {the Sorts of A}.i by PZFMISC1:def 1;
end;
hence thesis by PBOOLE:3;
end;
theorem Th31:
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A, B st F is_homomorphism A, B
holds MSHomQuot F ** MSNat_Hom(A,MSCng F) = F
proof
let A, B be non-empty MSAlgebra over S,
F be ManySortedFunction of A, B such that
A1: F is_homomorphism A, B;
now
let i be set;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
QuotMSAlg (A,MSCng F) = MSAlgebra(# Class MSCng F, QuotCharact MSCng F
#)
by MSUALG_4:def 16;
then reconsider h = MSHomQuot(F,s) as Function of (Class MSCng F).s,
(the Sorts of B).s;
reconsider f = h * MSNat_Hom(A,MSCng F,s) as Function of
(the Sorts of A).s, (the Sorts of B).s;
A2: for c being Element of (the Sorts of A).s holds f.c = F.s.c
proof
let c be Element of (the Sorts of A).s;
thus f.c
= h.((MSNat_Hom(A,MSCng F,s)).c) by FUNCT_2:21
.= h.(Class((MSCng F).s,c)) by MSUALG_4:def 17
.= h.(Class(MSCng(F,s),c)) by A1,MSUALG_4:def 20
.= F.s.c by A1,MSUALG_4:def 21;
end;
thus (MSHomQuot F ** MSNat_Hom(A,MSCng F)).i
= ((MSHomQuot F).s) * ((MSNat_Hom(A,MSCng F)).s) by MSUALG_3:2
.= MSHomQuot(F,s) * ((MSNat_Hom(A,MSCng F)).s) by MSUALG_4:def 22
.= MSHomQuot(F,s) * MSNat_Hom(A,MSCng F,s) by MSUALG_4:def 18
.= F.i by A2,FUNCT_2:113;
end;
hence MSHomQuot F ** MSNat_Hom(A,MSCng F) = F by PBOOLE:3;
end;
theorem Th32:
for A being non-empty MSAlgebra over S
for C being MSCongruence of A
for s being SortSymbol of S
for a being Element of (the Sorts of QuotMSAlg (A,C)).s
ex x being Element of (the Sorts of A).s st a = Class(C,x)
proof
let A be non-empty MSAlgebra over S,
C be MSCongruence of A,
s be SortSymbol of S,
a be Element of (the Sorts of QuotMSAlg (A,C)).s;
QuotMSAlg (A,C) = MSAlgebra (#Class C, QuotCharact C#)
by MSUALG_4:def 16;
then a in (Class C).s;
then a in Class (C.s) by MSUALG_4:def 8;
then consider t being set such that
A1: t in (the Sorts of A).s and
A2: a = Class(C.s,t) by EQREL_1:def 5;
reconsider t as Element of (the Sorts of A).s by A1;
take t;
thus thesis by A2,MSUALG_4:def 7;
end;
theorem
for A being MSAlgebra over S
for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2
for i being Element of S
for x, y being Element of (the Sorts of A).i st [x,y] in C1.i
holds Class (C1,x) c= Class (C2,y) &
(A is non-empty implies Class (C1,y) c= Class (C2,x))
proof
let A be MSAlgebra over S,
C1, C2 be MSEquivalence-like ManySortedRelation of A such that
A1: C1 c= C2;
let i be Element of S,
x, y be Element of (the Sorts of A).i such that
A2: [x,y] in C1.i;
A3: C1.i c= C2.i by A1,PBOOLE:def 5;
field(C1.i) = (the Sorts of A).i by ORDERS_1:97;
then
A4: C1.i is_transitive_in (the Sorts of A).i by RELAT_2:def 16;
thus Class (C1,x) c= Class (C2,y)
proof
let q be set; assume
A5: q in Class (C1,x);
then q in Class(C1.i,x) by MSUALG_4:def 7;
then [q,x] in C1.i by EQREL_1:27;
then [q,y] in C1.i by A2,A4,A5,RELAT_2:def 8;
then q in Class(C2.i,y) by A3,EQREL_1:27;
hence q in Class (C2,y) by MSUALG_4:def 7;
end;
assume A is non-empty;
then reconsider B = A as non-empty MSAlgebra over S;
let q be set such that
A6: q in Class (C1,y);
field(C1.i) = (the Sorts of A).i by ORDERS_1:97;
then C1.i is_symmetric_in (the Sorts of B).i by RELAT_2:def 11;
then A7: [y,x] in C1.i by A2,RELAT_2:def 3;
q in Class(C1.i,y) by A6,MSUALG_4:def 7;
then [q,y] in C1.i by EQREL_1:27;
then [q,x] in C1.i by A4,A6,A7,RELAT_2:def 8;
then q in Class(C2.i,x) by A3,EQREL_1:27;
hence q in Class (C2,x) by MSUALG_4:def 7;
end;
theorem
for A being non-empty MSAlgebra over S, C being MSCongruence of A
for s being SortSymbol of S, x, y being Element of (the Sorts of A).s holds
(MSNat_Hom(A,C)).s.x = (MSNat_Hom(A,C)).s.y iff [x,y] in C.s
proof
let A be non-empty MSAlgebra over S,
C be MSCongruence of A,
s be SortSymbol of S,
x, y be Element of (the Sorts of A).s;
set f = (MSNat_Hom(A,C)).s,
g = MSNat_Hom(A,C,s);
A1: f = g by MSUALG_4:def 18;
hereby
assume
A2: (MSNat_Hom(A,C)).s.x = (MSNat_Hom(A,C)).s.y;
Class(C.s,x) = g.x by MSUALG_4:def 17
.= Class(C.s,y) by A1,A2,MSUALG_4:def 17;
hence [x,y] in C.s by EQREL_1:44;
end;
assume
A3: [x,y] in C.s;
thus (MSNat_Hom(A,C)).s.x = Class(C.s,x) by A1,MSUALG_4:def 17
.= Class(C.s,y) by A3,EQREL_1:44
.= (MSNat_Hom(A,C)).s.y by A1,MSUALG_4:def 17;
end;
Lm1:
now
let S be non empty non void ManySortedSign,
A be non-empty MSAlgebra over S,
C1, C2 be MSCongruence of A;
let G be ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg (A,C2) such that
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);
thus G is "onto"
proof
set sL = the Sorts of QuotMSAlg (A,C1),
sP = the Sorts of QuotMSAlg (A,C2);
let i be set;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
rng(G.s) c= sP.s by RELSET_1:12;
hence rng(G.i) c= sP.i;
let q be set such that
A2: q in sP.i;
QuotMSAlg (A,C2) = MSAlgebra (#Class C2, QuotCharact C2#)
by MSUALG_4:def 16;
then q in Class(C2.s) by A2,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 as Element of (the Sorts of A).s by A3;
A5: dom (G.s) = sL.s by FUNCT_2:def 1;
A6: QuotMSAlg (A,C1) = MSAlgebra (#Class C1, QuotCharact C1#)
by MSUALG_4:def 16;
Class(C1.s,a) in Class (C1.s) by EQREL_1:def 5;
then Class(C1,a) in Class (C1.s) by MSUALG_4:def 7;
then reconsider x = Class(C1,a) as Element of sL.s by A6,MSUALG_4:def 8;
G.s.x = Class(C2,a) by A1
.= Class(C2.s,a) by MSUALG_4:def 7;
hence q in rng(G.i) by A4,A5,FUNCT_1:def 5;
end;
end;
theorem Th35:
for A being non-empty MSAlgebra over 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 ** MSNat_Hom(A,C1) = MSNat_Hom(A,C2)
proof
let A be non-empty MSAlgebra over S,
C1, C2 be MSCongruence of A;
let G be ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg (A,C2) such that
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);
set sL = the Sorts of QuotMSAlg (A,C1);
now
let i be set;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A2: for c being Element of (the Sorts of A).s holds
((G.s) * (MSNat_Hom(A,C1).s)).c = MSNat_Hom(A,C2).s.c
proof
let c be Element of (the Sorts of A).s;
A3: QuotMSAlg (A,C1) = MSAlgebra (#Class C1, QuotCharact C1#)
by MSUALG_4:def 16;
Class(C1.s,c) in Class (C1.s) by EQREL_1:def 5;
then Class(C1,c) in Class (C1.s) by MSUALG_4:def 7;
then A4: Class(C1,c) is Element of sL.s by A3,MSUALG_4:def 8;
thus ((G.s) * (MSNat_Hom(A,C1).s)).c
= (G.s).(MSNat_Hom(A,C1).s.c) by FUNCT_2:21
.= (G.s).(MSNat_Hom(A,C1,s).c) by MSUALG_4:def 18
.= (G.s).Class(C1.s,c) by MSUALG_4:def 17
.= (G.s).Class(C1,c) by MSUALG_4:def 7
.= Class(C2,c) by A1,A4
.= Class(C2.s,c) by MSUALG_4:def 7
.= MSNat_Hom(A,C2,s).c by MSUALG_4:def 17
.= MSNat_Hom(A,C2).s.c by MSUALG_4:def 18;
end;
thus (G ** MSNat_Hom(A,C1)).i
= (G.s) * (MSNat_Hom(A,C1).s) by MSUALG_3:2
.= MSNat_Hom(A,C2).i by A2,FUNCT_2:113;
end;
hence G ** MSNat_Hom(A,C1) = MSNat_Hom(A,C2) by PBOOLE:3;
end;
theorem Th36:
for A being non-empty MSAlgebra over 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)
proof
let A be non-empty MSAlgebra over S,
C1, C2 be MSCongruence of A;
let G be ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg (A,C2) such that
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);
A2: MSNat_Hom(A,C1) is_epimorphism A, QuotMSAlg (A,C1) by MSUALG_4:3;
MSNat_Hom(A,C2) is_epimorphism A, QuotMSAlg (A,C2) by MSUALG_4:3;
then A3: MSNat_Hom(A,C2) is_homomorphism A, QuotMSAlg (A,C2) by MSUALG_3:def 10
;
G ** MSNat_Hom(A,C1) = MSNat_Hom(A,C2) by A1,Th35;
hence G is_homomorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) by A2,A3,Th20;
thus G is "onto" by A1,Lm1;
end;
theorem
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A, B st F is_homomorphism A, B
for C1 being MSCongruence of A st C1 c= MSCng F
ex H being ManySortedFunction of QuotMSAlg (A,C1), B st
H is_homomorphism QuotMSAlg (A,C1), B & F = H ** MSNat_Hom(A,C1)
proof
let A, B be non-empty MSAlgebra over S,
F be ManySortedFunction of A, B such that
A1: F is_homomorphism A, B;
let C1 be MSCongruence of A such that
A2: C1 c= MSCng F;
set G = MSNat_Hom(A,C1),
I = the carrier of S,
sQ = the Sorts of QuotMSAlg (A,C1),
sF = the Sorts of QuotMSAlg (A,MSCng F);
defpred P[set,set,set] means
ex s being Element of I, xx being Element of (the Sorts of A).s st
$3 = s & $2 = Class(C1,xx) & $1 = Class(MSCng F,xx);
A3: for i being set st i in I holds
for x being set st x in sQ.i ex y being set st y in sF.i & P[y,x,i]
proof
let i be set;
assume i in I;
then reconsider s = i as Element of I;
let x be set;
assume x in sQ.i;
then consider x1 being Element of (the Sorts of A).s such that
A4: x = Class(C1,x1) by Th32;
take y = Class(MSCng F,x1);
y = Class((MSCng F).s,x1) by MSUALG_4:def 7;
then A5: y in Class ((MSCng F).s) by EQREL_1:def 5;
QuotMSAlg (A,MSCng F) = MSAlgebra (#Class MSCng F, QuotCharact MSCng F
#)
by MSUALG_4:def 16;
hence y in sF.i by A5,MSUALG_4:def 8;
thus P[y,x,i] by A4;
end;
consider C12 being ManySortedFunction of sQ, sF such that
A6: for i being set st i in I holds
ex f being Function of sQ.i, sF.i st f = C12.i &
for x being set st x in sQ.i holds P[f.x,x,i] from MSFExFunc(A3);
A7: 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
C12.i.x = Class(MSCng F,xx)
proof
let i be Element of S,
x be Element of (the Sorts of QuotMSAlg (A,C1)).i,
xx be Element of (the Sorts of A).i such that
A8: x = Class(C1,xx);
consider f being Function of sQ.i, sF.i such that
A9: f = C12.i and
A10: for x being set st x in sQ.i holds P[f.x,x,i] by A6;
consider s being Element of I,
x1 being Element of (the Sorts of A).s such that
A11: i = s and
A12: x = Class(C1,x1) and
A13: f.x = Class(MSCng F,x1) by A10;
A14: C1.s c= (MSCng F).s by A2,PBOOLE:def 5;
Class(C1.s,x1) = Class(C1,x1) by MSUALG_4:def 7
.= Class(C1.s,xx) by A8,A11,A12,MSUALG_4:def 7;
then xx in Class(C1.s,x1) by EQREL_1:31;
then [xx,x1] in C1.s by EQREL_1:27;
then A15: xx in Class((MSCng F).s,x1) by A14,EQREL_1:27;
thus C12.i.x = Class((MSCng F).s, x1) by A9,A13,MSUALG_4:def 7
.= Class((MSCng F).i, xx) by A11,A15,EQREL_1:31
.= Class(MSCng F, xx) by MSUALG_4:def 7;
end;
then C12 is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,MSCng F) by Th36;
then A16: C12 is_homomorphism QuotMSAlg (A,C1), QuotMSAlg (A,MSCng F)
by MSUALG_3:def 10;
reconsider H = MSHomQuot F**C12
as ManySortedFunction of QuotMSAlg (A,C1), B;
take H;
MSHomQuot F is_monomorphism QuotMSAlg (A,MSCng F), B by A1,MSUALG_4:4;
then MSHomQuot F is_homomorphism QuotMSAlg (A,MSCng F), B by MSUALG_3:def
11;
hence H is_homomorphism QuotMSAlg (A,C1), B by A16,MSUALG_3:10;
A17: now
let i be set;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A18: for x being Element of (the Sorts of A).s holds
(C12.s * G.s).x = (MSNat_Hom(A,MSCng F)).s.x
proof
let x be Element of (the Sorts of A).s;
Class(C1.s,x) in Class (C1.s) by EQREL_1:def 5;
then Class(C1,x) in Class (C1.s) by MSUALG_4:def 7;
then A19: Class(C1,x) in (Class C1).s by MSUALG_4:def 8;
A20: QuotMSAlg (A,C1) = MSAlgebra (#Class C1, QuotCharact C1#)
by MSUALG_4:def 16;
thus (C12.s * G.s).x
= C12.s.(G.s.x) by FUNCT_2:21
.= C12.s.(MSNat_Hom(A,C1,s).x) by MSUALG_4:def 18
.= C12.s.(Class(C1.s,x)) by MSUALG_4:def 17
.= C12.s.(Class(C1,x)) by MSUALG_4:def 7
.= Class(MSCng F,x) by A7,A19,A20
.= Class((MSCng F).s,x) by MSUALG_4:def 7
.= MSNat_Hom(A,MSCng F,s).x by MSUALG_4:def 17
.= (MSNat_Hom(A,MSCng F)).s.x by MSUALG_4:def 18;
end;
thus (C12 ** G).i = C12.s * G.s by MSUALG_3:2
.= (MSNat_Hom(A,MSCng F)).i by A18,FUNCT_2:113;
end;
thus F = MSHomQuot F ** MSNat_Hom(A,MSCng F) by A1,Th31
.= MSHomQuot F ** (C12 ** G) by A17,PBOOLE:3
.= H ** MSNat_Hom(A,C1) by AUTALG_1:13;
end;