Copyright (c) 1994 Association of Mizar Users
environ
vocabulary AMI_1, MSUALG_1, PBOOLE, PRALG_1, FUNCT_1, RELAT_1, BOOLE,
ZF_REFLE, QC_LANG1, TDGROUP, FUNCT_6, FUNCT_5, FINSEQ_4, ALG_1, CARD_3,
GROUP_6, WELLORD1, MSUALG_2, UNIALG_2, MSUALG_3;
notation TARSKI, XBOOLE_0, SUBSET_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, FINSEQ_1, CARD_3, FINSEQ_4, FUNCT_5, FUNCT_6, PBOOLE, STRUCT_0,
PRALG_1, MSUALG_1, MSUALG_2, PRALG_2;
constructors FINSEQ_4, MSUALG_2, PRALG_2, MEMBERED, PARTFUN1, RELAT_2,
XBOOLE_0;
clusters FUNCT_1, PBOOLE, MSUALG_1, MSUALG_2, PRALG_1, RELSET_1, STRUCT_0,
MEMBERED, ZFMISC_1, PARTFUN1, FUNCT_2, XBOOLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, MSUALG_2, XBOOLE_0;
theorems FUNCT_1, FUNCT_2, FINSEQ_1, PBOOLE, CARD_3, MSUALG_1, PRALG_1,
FINSEQ_4, MSUALG_2, TARSKI, RELAT_1, PRALG_2, FUNCT_6, FUNCT_5, FINSEQ_2,
RELSET_1, XBOOLE_0;
schemes FUNCT_1, ZFREFLE1;
begin
reserve S for non void non empty ManySortedSign,
U1,U2 for MSAlgebra over S,
o for OperSymbol of S,
n for Nat;
:::::::::::::::::::::::::::::::::::::::::::::::::
:: ::
:: PRELIMINARIES - MANY SORTED FUNCTIONS ::
:: ::
:::::::::::::::::::::::::::::::::::::::::::::::::
definition let I be non empty set,
A,B be ManySortedSet of I,
F be ManySortedFunction of A,B,
i be Element of I;
redefine func F.i -> Function of A.i,B.i;
coherence by MSUALG_1:def 2;
end;
definition let S; let U1,U2 be MSAlgebra over S;
mode ManySortedFunction of U1,U2 is
ManySortedFunction of the Sorts of U1, the Sorts of U2;
end;
definition let I be set,A be ManySortedSet of I;
func id A -> ManySortedFunction of A,A means :Def1:
for i be set st i in I holds it.i = id (A.i);
existence
proof
deffunc F(set)=id (A.$1);
consider f being Function such that
A1: dom f = I & for i be set st i in I holds f.i = F(i) from Lambda;
reconsider f as ManySortedSet of I by A1,PBOOLE:def 3;
for x be set st x in dom f holds f.x is Function
proof
let x be set;
assume x in dom f;
then f.x = id (A.x) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of I by PRALG_1:def 15;
for i be set st i in I holds f.i is Function of A.i,A.i
proof
let i be set;
assume i in I;
then f.i = id (A.i) by A1;
hence thesis;
end;
then reconsider f as ManySortedFunction of A,A by MSUALG_1:def 2;
take f;
thus thesis by A1;
end;
uniqueness
proof
let F,G be ManySortedFunction of A,A;
assume that
A2: for i be set st i in I holds F.i = id (A.i) and
A3: for i be set st i in I holds G.i = id (A.i);
A4: dom F = I & dom G = I by PBOOLE:def 3;
now
let i be set;
assume i in I;
then F.i = id (A.i) & G.i = id (A.i) by A2,A3;
hence F.i = G.i;
end;
hence thesis by A4,FUNCT_1:9;
end;
end;
definition let IT be Function;
attr IT is "1-1" means :Def2:
for i be set, f be Function st i in dom IT & IT.i = f holds f is one-to-one;
end;
definition let I be set;
cluster "1-1" ManySortedFunction of I;
existence
proof
consider A be ManySortedSet of I;
take F = id A;
let i be set, f be Function;
assume A1: i in dom F & F.i = f;
dom (id A) = I by PBOOLE:def 3;
then f = id (A.i) by A1,Def1;
hence thesis;
end;
end;
theorem Th1:
for I be set,F be ManySortedFunction of I holds
F is "1-1" iff
for i be set st i in I holds F.i is one-to-one
proof
let I be set;
let F be ManySortedFunction of I;
A1: dom F = I by PBOOLE:def 3;
hence F is "1-1" implies for i be set st i in I holds F.i is one-to-one
by Def2;
assume for i be set st i in I holds F.i is one-to-one;
then for i be set, f being Function st i in dom F & f = F.i
holds f is one-to-one by A1;
hence F is "1-1" by Def2;
end;
definition let I be set, A,B be ManySortedSet of I;
let IT be ManySortedFunction of A,B;
attr IT is "onto" means :Def3:
for i be set st i in I holds rng(IT.i) = B.i;
end;
definition
let F,G be Function-yielding Function;
func G**F -> Function-yielding Function means :Def4:
dom it = (dom F) /\ (dom G) &
for i be set st i in dom it holds it.i = (G.i)*(F.i);
existence
proof
defpred P[set,set] means $2 = (G.$1)*(F.$1);
A1: for i be set st i in dom F /\ dom G ex u be set st P[i,u];
consider H being Function such that
A2: dom H = dom F /\ dom G & for i be set st i in dom F /\ dom G holds
P[i,H.i] from NonUniqFuncEx(A1);
for x be set st x in dom H holds H.x is Function
proof
let x be set;
assume A3: x in dom H;
reconsider f = F.x as Function;
reconsider g = G.x as Function;
H.x = g*f by A2,A3;
hence thesis;
end;
then reconsider H as Function-yielding Function by PRALG_1:def 15;
take H;
thus thesis by A2;
end;
uniqueness
proof
let H1,H2 be Function-yielding Function;
assume that
A4: dom H1 = dom F /\ dom G & for i be set st i in dom H1
holds H1.i = (G.i)*(F.i) and
A5: dom H2 = dom F /\ dom G & for i be set st i in dom H2
holds H2.i = (G.i)*(F.i);
now
let i be set;
assume A6: i in dom F /\ dom G;
reconsider f = F.i as Function;
reconsider g = G.i as Function;
H1.i = g*f & H2.i = g*f by A4,A5,A6;
hence H1.i = H2.i;
end;
hence thesis by A4,A5,FUNCT_1:9;
end;
end;
theorem Th2:
for I be set, A,B,C be ManySortedSet of I,
F be ManySortedFunction of A,B, G be ManySortedFunction of B,C holds
dom (G ** F) = I &
for i be set st i in I holds (G**F).i = (G.i)*(F.i)
proof
let I be set,
A,B,C be ManySortedSet of I,
F be ManySortedFunction of A,B,
G be ManySortedFunction of B,C;
dom F = I & dom G = I by PBOOLE:def 3;
then (dom F) /\ (dom G) = I;
hence A1: dom (G ** F) = I by Def4;
let i be set;
thus thesis by A1,Def4;
end;
definition let I be set,
A be ManySortedSet of I,
B,C be non-empty ManySortedSet of I,
F be ManySortedFunction of A,B,
G be ManySortedFunction of B,C;
redefine func G**F -> ManySortedFunction of A,C;
coherence
proof
dom (G ** F) = I by Th2;
then reconsider fg = G ** F as ManySortedSet of I by PBOOLE:def 3;
reconsider fg as ManySortedFunction of I;
for i be set st i in I holds fg.i is Function of A.i,C.i
proof
let i be set;
assume A1: i in I;
then reconsider f = F.i as Function of A.i,B.i by MSUALG_1:def 2;
reconsider g = G.i as Function of B.i,C.i by A1,MSUALG_1:def 2;
A2: (G**F).i = g*f by A1,Th2;
B.i = {} implies A.i = {} by A1,PBOOLE:def 16;
then A3: dom f = A.i & rng f c= B.i by FUNCT_2:def 1,RELSET_1:12;
C.i = {} implies B.i = {} by A1,PBOOLE:def 16;
then A4: dom g = B.i & rng g c= C.i by FUNCT_2:def 1,RELSET_1:12;
A5: dom (g*f) = A.i by A3,A4,RELAT_1:46;
C.i = {} implies A.i = {} by A1,PBOOLE:def 16;
hence thesis by A2,A5,FUNCT_2:def 1;
end; hence thesis by MSUALG_1:def 2;
end;
end;
theorem
for I be set,A,B be ManySortedSet of I,
F be ManySortedFunction of A,B holds F**(id A) = F
proof
let I be set,
A,B be ManySortedSet of I,
F be ManySortedFunction of A,B;
dom (F**(id A)) = (dom F) /\ dom id A by Def4 .= I /\
dom id A by PBOOLE:def 3
.= I /\ I by PBOOLE:def 3 .= I;
then reconsider G = F**(id A) as ManySortedFunction of I by PBOOLE:def 3;
now
let i be set; assume A1: i in I;
then reconsider f = F.i as Function of A.i,B.i by MSUALG_1:def 2;
reconsider g = (id A).i as Function of A.i,A.i by A1,MSUALG_1:def 2;
A2: G.i = f*g by A1,Th2 .= f*(id (A.i)) by A1,Def1;
per cases; suppose
B.i = {} implies A.i = {};
then dom f = A.i by FUNCT_2:def 1;
hence G.i = F.i by A2,FUNCT_1:42;
suppose B.i = {} & A.i <> {}; then f = {} by FUNCT_2:def 1;
hence G.i = F.i by A2,RELAT_1:62;
end;
hence thesis by PBOOLE:3;
end;
theorem Th4:
for I be set, A,B be ManySortedSet of I
for F be ManySortedFunction of A, B holds (id B)**F = F
proof
let I be set;
let A,B be ManySortedSet of I;
let F be ManySortedFunction of A, B;
dom ((id B)**F) = (dom id B) /\ dom F by Def4 .= I /\
dom F by PBOOLE:def 3
.= I /\ I by PBOOLE:def 3 .= I;
then reconsider G = (id B)**F as ManySortedFunction of I by PBOOLE:def 3;
now let i be set; assume
A1: i in I;
then reconsider f = F.i as Function of A.i, B.i by MSUALG_1:def 2;
reconsider g = (id B).i as Function of B.i, B.i by A1,MSUALG_1:def 2;
A2: g = id (B.i) by A1,Def1;
A3: G.i = g * f by A1,Th2;
per cases; suppose
B.i = {} implies A.i = {};
hence G.i = F.i by A2,A3,FUNCT_2:23;
suppose B.i = {} & A.i <> {}; then f = {} by FUNCT_2:def 1;
hence G.i = F.i by A3,RELAT_1:62;
end;
hence (id B)**F = F by PBOOLE:3;
end;
definition let I be set,
A,B be ManySortedSet of I,
F be ManySortedFunction of A,B;
assume A1: F is "1-1" & F is "onto";
func F"" -> ManySortedFunction of B,A means :Def5:
for i be set st i in I holds it.i = (F.i)";
existence
proof
defpred P[set,set] means $2 = (F.$1)";
A2: for i be set st i in I ex u be set st P[i,u];
consider H being Function such that
A3: dom H = I & for i be set st i in I holds P[i,H.i] from NonUniqFuncEx(A2);
reconsider H as ManySortedSet of I by A3,PBOOLE:def 3;
for x be set st x in dom H holds H.x is Function
proof
let x be set;
assume A4: x in dom H;
then x in I by PBOOLE:def 3;
then reconsider f = F.x as Function of A.x,B.x by MSUALG_1:def 2;
H.x = f" by A3,A4;
hence thesis;
end;
then reconsider H as ManySortedFunction of I by PRALG_1:def 15;
for i be set st i in I holds H.i is Function of B.i,A.i
proof
let i be set;
assume A5: i in I;
then A6: i in dom F by PBOOLE:def 3;
reconsider f = F.i as Function of A.i,B.i by A5,MSUALG_1:def 2;
A7: f is one-to-one by A1,A6,Def2;
rng f = B.i by A1,A5,Def3;
then f" is Function of B.i,A.i by A7,FUNCT_2:31;
hence thesis by A3,A5;
end;
then reconsider H as ManySortedFunction of B,A by MSUALG_1:def 2;
take H;
thus thesis by A3;
end;
uniqueness
proof
let H1,H2 be ManySortedFunction of B,A;
assume that
A8: for i be set st i in I holds H1.i = (F.i)" and
A9: for i be set st i in I holds H2.i = (F.i)";
now
let i be set;
assume A10: i in I;
then reconsider f = F.i as Function of A.i,B.i by MSUALG_1:def 2;
H1.i = f" & H2.i = f" by A8,A9,A10;
hence H1.i = H2.i;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem Th5:
for I be set,A,B be non-empty ManySortedSet of I,
H be ManySortedFunction of A,B, H1 be ManySortedFunction of B,A st
H is "1-1" "onto" & H1 = H"" holds H**H1 = id B & H1**H = id A
proof
let I be set,
A,B be non-empty ManySortedSet of I,
H be ManySortedFunction of A,B,
H1 be ManySortedFunction of B,A;
assume A1: H is "1-1" "onto" & H1 = H"";
A2: for i be set st i in I holds (H1**H).i = id (A.i)
proof
let i be set; assume A3: i in I;
then A4:i in dom H by PBOOLE:def 3;
reconsider h = H.i as Function of A.i,B.i by A3,MSUALG_1:def 2;
reconsider h1 = H1.i as Function of B.i,A.i by A3,MSUALG_1:def 2;
A5: h1 = h" by A1,A3,Def5;
A6: h is one-to-one by A1,A4,Def2;
B.i = {} implies A.i = {} by A3,PBOOLE:def 16;
then dom h = A.i & rng h c= B.i by FUNCT_2:def 1,RELSET_1:12;
then h1*h = id (A.i) by A5,A6,FUNCT_1:61;
hence thesis by A3,Th2;
end;
now
let i be set; assume A7: i in I;
then A8:i in dom H by PBOOLE:def 3;
reconsider h = H.i as Function of A.i,B.i by A7,MSUALG_1:def 2;
reconsider h1 = H1.i as Function of B.i,A.i by A7,MSUALG_1:def 2;
A9: h1 = h" by A1,A7,Def5;
h is one-to-one by A1,A8,Def2;
then h*h1 = id rng h by A9,FUNCT_1:61;
then h*h1 = id (B.i) by A1,A7,Def3;
hence (H**H1).i = id (B.i) by A7,Th2;
end;
hence thesis by A2,Def1;
end;
definition let I be set,
A be ManySortedSet of I,
F be ManySortedFunction of I;
func F.:.:A -> ManySortedSet of I means :Def6:
for i be set st i in I holds it.i = (F.i).:(A.i);
existence
proof
defpred P[set,set] means $2 = (F.$1).:(A.$1);
A1: for i be set st i in I ex u be set st P[i,u];
consider g being Function such that A2: dom g = I & for i be set st i in I
holds P[i,g.i] from NonUniqFuncEx(A1);
reconsider g as ManySortedSet of I by A2,PBOOLE:def 3;
take g;
thus thesis by A2;
end;
uniqueness
proof
let B,B1 be ManySortedSet of I;
assume that
A3: for i be set st i in I holds B.i = (F.i).:(A.i) and
A4: for i be set st i in I holds B1.i = (F.i).:(A.i);
now
let i be set;
assume A5: i in I;
reconsider f = F.i as Function;
B.i = f.:(A.i) & B1.i = f.:(A.i) by A3,A4,A5;
hence B.i = B1.i;
end;
hence thesis by PBOOLE:3;
end;
end;
Lm1:
now let S; let U1 be MSAlgebra over S; let o;
let x be set; assume x in Args(o,U1);
then x in product((the Sorts of U1) * (the_arity_of o)) by PRALG_2:10;
then ex f being Function st x = f &
dom f = dom ((the Sorts of U1) * (the_arity_of o)) & for y be set st
y in dom ((the Sorts of U1) * (the_arity_of o)) holds
f.y in ((the Sorts of U1) * (the_arity_of o)).y by CARD_3:def 5;
hence x is Function;
end;
definition let S; let U1 be non-empty MSAlgebra over S; let o;
cluster -> Function-like Relation-like Element of Args(o,U1);
coherence by Lm1;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::
:: ::
:: HOMOMORPHISMS OF MANY SORTED ALGEBRAS ::
:: ::
:::::::::::::::::::::::::::::::::::::::::::::::
theorem Th6:
for U1 being MSAlgebra over S
for x be Function st x in Args(o,U1) holds dom x = dom (the_arity_of o) &
for y be set st y in dom ((the Sorts of U1) * (the_arity_of o)) holds
x.y in ((the Sorts of U1) * (the_arity_of o)).y
proof let U1 be MSAlgebra over S;
let x be Function; assume A1: x in Args(o,U1);
A2: Args(o,U1) = product((the Sorts of U1) * (the_arity_of o)) by PRALG_2:10;
then A3: dom x = dom ((the Sorts of U1) * (the_arity_of o)) by A1,CARD_3:18;
dom (the Sorts of U1) = (the carrier of S) by PBOOLE:def 3;
then rng (the_arity_of o) c= dom (the Sorts of U1) by FINSEQ_1:def 4;
hence thesis by A1,A2,A3,CARD_3:18,RELAT_1:46;
end;
definition let S; let U1,U2 be MSAlgebra over S; let o;
let F be ManySortedFunction of U1,U2;
let x be Element of Args(o,U1);
assume that
A1: Args(o,U1) <> {} and
A2: Args(o,U2) <> {};
func F # x -> Element of Args(o,U2) equals :Def7:
(Frege(F*the_arity_of o)).x;
coherence
proof
A3: rng the_arity_of o c= the carrier of S by FINSEQ_1:def 4;
then A4: rng the_arity_of o c= dom the Sorts of U2 by PBOOLE:def 3;
A5: rng the_arity_of o c= dom F by A3,PBOOLE:def 3;
x in Args(o,U1) by A1;
then A6: x in product((the Sorts of U1) * (the_arity_of o)) by PRALG_2:10;
A7: dom((the Sorts of U1)*(the_arity_of o))
= (F*the_arity_of o)"SubFuncs rng(F*the_arity_of o)
proof
hereby
let e be set;
assume
A8: e in dom((the Sorts of U1)*(the_arity_of o));
then A9: e in dom the_arity_of o by FUNCT_1:21;
(the_arity_of o).e in dom the Sorts of U1 by A8,FUNCT_1:21;
then (the_arity_of o).e in the carrier of S by PBOOLE:def 3;
then (the_arity_of o).e in dom F by PBOOLE:def 3;
then A10: e in dom(F*the_arity_of o) by A9,FUNCT_1:21;
(F*the_arity_of o).e is Function;
hence e in (F*the_arity_of o)"SubFuncs rng(F*the_arity_of o)
by A10,FUNCT_6:28;
end;
let e be set;
assume e in (F*the_arity_of o)"SubFuncs rng(F*the_arity_of o);
then e in dom(F*the_arity_of o) by FUNCT_6:28;
then A11: e in dom the_arity_of o by FUNCT_1:21;
then (the_arity_of o).e in the carrier of S by FINSEQ_2:13;
then (the_arity_of o).e in dom the Sorts of U1 by PBOOLE:def 3;
hence e in dom((the Sorts of U1)*(the_arity_of o)) by A11,FUNCT_1:21;
end;
now let e be set;
assume e in (F*the_arity_of o)"SubFuncs rng(F*the_arity_of o);
then e in dom(F*the_arity_of o) by FUNCT_6:28;
then A12: e in dom the_arity_of o by FUNCT_1:21;
then A13: (the_arity_of o).e in the carrier of S by FINSEQ_2:13;
then (the_arity_of o).e in dom the Sorts of U2 by PBOOLE:def 3;
then A14: e in dom((the Sorts of U2)*(the_arity_of o)) by A12,FUNCT_1:21;
reconsider Foe = F.((the_arity_of o).e) as
Function of (the Sorts of U1).((the_arity_of o).e),
(the Sorts of U2).((the_arity_of o).e) by A13,MSUALG_1:def 2;
A15: ((the Sorts of U2)*(the_arity_of o)).e
= (the Sorts of U2).((the_arity_of o).e) by A12,FUNCT_1:23;
A16: product((the Sorts of U2)*(the_arity_of o)) <> {} by A2,PRALG_2:10;
A17: now assume (the Sorts of U2).((the_arity_of o).e) = {};
then {}
in rng((the Sorts of U2)*(the_arity_of o)) by A14,A15,FUNCT_1:def 5;
hence contradiction by A16,CARD_3:37;
end;
thus ((the Sorts of U1)*(the_arity_of o)).e
= (the Sorts of U1).((the_arity_of o).e) by A12,FUNCT_1:23
.= dom Foe by A17,FUNCT_2:def 1
.= proj1 Foe by FUNCT_5:21
.= proj1 ((F*the_arity_of o).e) by A12,FUNCT_1:23;
end;
then A18: (the Sorts of U1) * (the_arity_of o) = doms(F*the_arity_of o)
by A7,FUNCT_6:def 2;
then consider f being Function such that
A19: x = f and dom f = dom doms(F*the_arity_of o) and
A20: for e being set st e in dom doms(F*the_arity_of o)
holds f.e in ( doms(F*the_arity_of o)).e by A6,CARD_3:def 5;
A21: (Frege(F*the_arity_of o)).x = (F*the_arity_of o)..f by A6,A18,A19,PRALG_2
:def 8;
A22: dom((F*the_arity_of o)..f) = dom(F*the_arity_of o) by PRALG_1:def 18;
A23: dom(F*the_arity_of o) = dom the_arity_of o by A5,RELAT_1:46
.= dom((the Sorts of U2)*(the_arity_of o)) by A4,RELAT_1:46;
now let e be set;
assume
A24: e in dom((the Sorts of U2)*(the_arity_of o));
then A25: e in dom the_arity_of o by FUNCT_1:21;
then A26: (the_arity_of o).e in the carrier of S by FINSEQ_2:13;
then reconsider g = F.((the_arity_of o).e) as
Function of (the Sorts of U1).((the_arity_of o).e),
(the Sorts of U2).((the_arity_of o).e) by MSUALG_1:def 2;
g = (F*the_arity_of o).e by A23,A24,FUNCT_1:22;
then A27: ((F*the_arity_of o)..f).e = g.(f.e) by A23,A24,PRALG_1:def
18;
A28: ((the Sorts of U2)*(the_arity_of o)).e
= (the Sorts of U2).((the_arity_of o).e) by A25,FUNCT_1:23;
A29: product((the Sorts of U2)*(the_arity_of o)) <> {} by A2,PRALG_2:10;
A30: now assume (the Sorts of U2).((the_arity_of o).e) = {};
then {}
in rng((the Sorts of U2)*(the_arity_of o)) by A24,A28,FUNCT_1:def 5;
hence contradiction by A29,CARD_3:37;
end;
(the_arity_of o).e in dom the Sorts of U1 by A26,PBOOLE:def 3;
then e in dom((the Sorts of U1)*(the_arity_of o)) by A25,FUNCT_1:21;
then f.e in (doms(F*the_arity_of o)).e by A18,A20;
then f.e in (the Sorts of U1).((the_arity_of o).e) by A18,A25,FUNCT_1:23
;
then g.(f.e) in (the Sorts of U2).((the_arity_of o).e) by A30,FUNCT_2:7;
hence ((F*the_arity_of o)..f).e in ((the Sorts of U2)*(the_arity_of o)).e
by A24,A27,FUNCT_1:22;
end;
then (Frege(F*the_arity_of o)).x in product((the Sorts of U2)*(
the_arity_of o))
by A21,A22,A23,CARD_3:18;
hence thesis by PRALG_2:10;
end;
correctness;
end;
Lm2:
now let S; let U1,U2 be MSAlgebra over S; let o;
let F be ManySortedFunction of U1,U2;
let x be Element of Args(o,U1), f,u be Function;
assume A1: x = f & x in Args(o,U1) & u in Args(o,U2);
A2: rng the_arity_of o c= the carrier of S by FINSEQ_1:def 4;
then A3: rng the_arity_of o c= dom the Sorts of U1 by PBOOLE:def 3;
A4: Args(o,U1) = product((the Sorts of U1) * (the_arity_of o)) &
Args(o,U2) = product((the Sorts of U2) * (the_arity_of o))
by PRALG_2:10;
then A5: dom f = dom((the Sorts of U1) * (the_arity_of o)) by A1,CARD_3:18
.= dom the_arity_of o by A3,RELAT_1:46;
A6: rng the_arity_of o c= dom the Sorts of U2 by A2,PBOOLE:def 3;
A7: dom u = dom((the Sorts of U2) * (the_arity_of o)) by A1,A4,CARD_3:18;
then A8: dom u = dom the_arity_of o by A6,RELAT_1:46;
A9: dom((the Sorts of U1)*(the_arity_of o))
= (F*the_arity_of o)"SubFuncs rng(F*the_arity_of o)
proof
hereby
let e be set;
assume
A10: e in dom((the Sorts of U1)*(the_arity_of o));
then A11: e in dom the_arity_of o by FUNCT_1:21;
(the_arity_of o).e in dom the Sorts of U1 by A10,FUNCT_1:21;
then (the_arity_of o).e in the carrier of S by PBOOLE:def 3;
then (the_arity_of o).e in dom F by PBOOLE:def 3;
then A12: e in dom(F*the_arity_of o) by A11,FUNCT_1:21;
(F*the_arity_of o).e is Function;
hence e in (F*the_arity_of o)"SubFuncs rng(F*the_arity_of o)
by A12,FUNCT_6:28;
end;
let e be set;
assume e in (F*the_arity_of o)"SubFuncs rng(F*the_arity_of o);
then e in dom(F*the_arity_of o) by FUNCT_6:28;
then A13: e in dom the_arity_of o by FUNCT_1:21;
then (the_arity_of o).e in the carrier of S by FINSEQ_2:13;
then (the_arity_of o).e in dom the Sorts of U1 by PBOOLE:def 3;
hence e in dom((the Sorts of U1)*(the_arity_of o)) by A13,FUNCT_1:21;
end;
now let e be set;
assume e in (F*the_arity_of o)"SubFuncs rng(F*the_arity_of o);
then e in dom(F*the_arity_of o) by FUNCT_6:28;
then A14: e in dom the_arity_of o by FUNCT_1:21;
then (the_arity_of o).e in the carrier of S by FINSEQ_2:13;
then reconsider Foe = F.((the_arity_of o).e) as
Function of (the Sorts of U1).((the_arity_of o).e),
(the Sorts of U2).((the_arity_of o).e) by MSUALG_1:def 2;
A15: ((the Sorts of U1)*(the_arity_of o)).e
= (the Sorts of U1).((the_arity_of o).e) &
((the Sorts of U2)*(the_arity_of o)).e
= (the Sorts of U2).((the_arity_of o).e) by A14,FUNCT_1:23;
((the Sorts of U2)*the_arity_of o).e in
rng ((the Sorts of U2)*the_arity_of o) by A7,A8,A14,FUNCT_1:def 5
;
then ((the Sorts of U2)*the_arity_of o).e <> {} by A1,A4,CARD_3:37;
hence ((the Sorts of U1)*(the_arity_of o)).e
= dom Foe by A15,FUNCT_2:def 1
.= proj1 Foe by FUNCT_5:21
.= proj1 ((F*the_arity_of o).e) by A14,FUNCT_1:23;
end;
then A16: (the Sorts of U1) * (the_arity_of o) = doms(F*the_arity_of o)
by A9,FUNCT_6:def 2;
hereby assume u = F#x;
then A17: u = (Frege(F*the_arity_of o)).x by A1,Def7;
let n;
assume
A18: n in dom f;
then (the_arity_of o).n in the carrier of S by A5,FINSEQ_2:13;
then (the_arity_of o).n in dom F by PBOOLE:def 3;
then A19: n in dom(F*the_arity_of o) by A5,A18,FUNCT_1:21;
then A20: (F*the_arity_of o).n = F.((the_arity_of o).n) by FUNCT_1:22
.= F.((the_arity_of o)/.n) by A5,A18,FINSEQ_4:def 4;
thus u.n = ((F*the_arity_of o)..f).n by A1,A4,A16,A17,PRALG_2:def 8
.= (F.((the_arity_of o)/.n)).(f.n) by A19,A20,PRALG_1:def 18;
end;
assume
A21: for n st n in dom f holds u.n = (F.((the_arity_of o)/.n)).(f.n);
A22: rng the_arity_of o c= dom F by A2,PBOOLE:def 3;
reconsider g = F#x as Function by A1,Lm1;
A23: F#x = (Frege(F*the_arity_of o)).x by A1,Def7;
then F#x = (F*the_arity_of o)..f by A1,A4,A16,PRALG_2:def 8;
then A24: dom g = dom(F*the_arity_of o) by PRALG_1:def 18
.= dom f by A5,A22,RELAT_1:46;
now let e be set;
assume
A25: e in dom f;
then reconsider n = e as Nat by A5;
(the_arity_of o).n in the carrier of S by A5,A25,FINSEQ_2:13;
then (the_arity_of o).n in dom F by PBOOLE:def 3;
then A26: n in dom(F*the_arity_of o) by A5,A25,FUNCT_1:21;
then A27: (F*the_arity_of o).n = F.((the_arity_of o).n) by FUNCT_1:22
.= (F.((the_arity_of o)/.n)) by A5,A25,FINSEQ_4:def 4;
thus u.e = (F.((the_arity_of o)/.n)).(f.n) by A21,A25
.= ((F*the_arity_of o)..f).n by A26,A27,PRALG_1:def 18
.= g.e by A1,A4,A16,A23,PRALG_2:def 8;
end;
hence u = F#x by A5,A8,A24,FUNCT_1:9;
end;
definition let S; let U1 be non-empty MSAlgebra over S; let o;
cluster Function-like Relation-like Element of Args(o,U1);
existence
proof consider x being Element of Args(o,U1);
x is Function-like Relation-like;
hence thesis;
end;
end;
definition let S; let U1,U2 be non-empty MSAlgebra over S; let o;
let F be ManySortedFunction of U1,U2;
let x be Element of Args(o,U1);
redefine func F # x -> Function-like Relation-like Element of Args(o,U2 )
means :Def8:
for n st n in dom x holds it.n = (F.((the_arity_of o)/.n)).(x.n);
coherence;
compatibility by Lm2;
end;
theorem Th7:
for S,o for U1 being MSAlgebra over S st Args(o,U1) <> {}
for x be Element of Args(o,U1) holds
x = ((id (the Sorts of U1))#x)
proof
let S,o; let U1 be MSAlgebra over S; assume
A1: Args(o,U1) <> {};
then reconsider AA = Args(o,U1) as non empty set;
let x be Element of Args(o,U1);
A2: Args(o,U1) = product((the Sorts of U1) * (the_arity_of o))
by PRALG_2:10;
then consider f being Function such that
A3: x = f and dom f = dom ((the Sorts of U1) * (the_arity_of o)) and
for x being set st x in dom ((the Sorts of U1)*the_arity_of o)
holds f.x in ((the Sorts of U1)*the_arity_of o).x by A1,CARD_3:def 5;
set F = id (the Sorts of U1);
reconsider Fx = F#x as Element of AA;
consider g being Function such that
A4: Fx = g and dom g = dom ((the Sorts of U1) * (the_arity_of o)) and
for x being set st x in dom ((the Sorts of U1)*the_arity_of o)
holds g.x in ((the Sorts of U1)*the_arity_of o).x by A2,CARD_3:def 5;
A5: dom f = dom (the_arity_of o) & dom g = dom (the_arity_of o)
by A3,A4,Th6;
for y be set st y in dom f holds f.y = g.y
proof
let y be set;
assume A6: y in dom f;
then reconsider n = y as Nat by A5;
A7: g.n = (F.((the_arity_of o)/.n)).(f.n) by A3,A4,A6,Lm2;
set p = ((the_arity_of o)/.n);
dom (the Sorts of U1) = (the carrier of S) by PBOOLE:def 3;
then rng (the_arity_of o) c= dom (the Sorts of U1) by FINSEQ_1:def 4;
then A8: dom ((the Sorts of U1)*(the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:46;
A9: F.p = id ((the Sorts of U1).p) by Def1;
f.n in ((the Sorts of U1) * (the_arity_of o)).n by A1,A3,A5,A6,A8,Th6;
then f.n in (the Sorts of U1).((the_arity_of o).n) by A5,A6,A8,FUNCT_1:22
;
then f.n in (the Sorts of U1).p by A5,A6,FINSEQ_4:def 4;
hence thesis by A7,A9,FUNCT_1:35;
end;
hence thesis by A3,A4,A5,FUNCT_1:9;
end;
theorem Th8:
for U1,U2,U3 being non-empty MSAlgebra over S
for H1 be ManySortedFunction of U1,U2, H2 be ManySortedFunction of U2,U3,
x be Element of Args(o,U1) holds (H2**H1)#x = H2#(H1#x)
proof let U1,U2,U3 be non-empty MSAlgebra over S;
let H1 be ManySortedFunction of U1,U2,H2 be ManySortedFunction of U2,U3;
let x be Element of Args(o,U1);
A1: dom ((H2**H1)#x) = dom (the_arity_of o) &
dom x = dom (the_arity_of o) &
dom (H2#(H1#x)) = dom (the_arity_of o) &
dom (H1#x) = dom (the_arity_of o) by Th6;
for y be set st y in dom (the_arity_of o) holds
((H2**H1)#x).y = ((H2#(H1#x))).y
proof
let y be set;
assume A2: y in dom (the_arity_of o);
then reconsider n = y as Nat;
set F = H2**H1,
p = ((the_arity_of o)/.n);
A3: (F#x).n = (F.p).(x.n) by A1,A2,Def8;
rng (the_arity_of o) c= (the carrier of S) by FINSEQ_1:def 4;
then rng (the_arity_of o) c= dom (the Sorts of U1) by PBOOLE:def 3;
then A4: dom ((the Sorts of U1)*(the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:46;
A5: p = (the_arity_of o).n by A2,FINSEQ_4:def 4;
A6: dom (H1.p) = (the Sorts of U1).p & rng (H1.p) c= (the Sorts of U2).p
by FUNCT_2:def 1,RELSET_1:12;
then A7: dom ((H2.p)*(H1.p)) = dom (H1.p) by FUNCT_2:def 1;
((the Sorts of U1) * (the_arity_of o)).n =(the Sorts of U1).p by A2,A4
,A5,FUNCT_1:22;
then A8: x.n in dom ((H2.p)*(H1.p)) by A2,A4,A6,A7,Th6;
F.p = (H2.p)*(H1.p) by Th2;
hence (F#x).y = (H2.p).((H1.p).(x.n)) by A3,A8,FUNCT_1:22
.= (H2.p).((H1#x).n) by A1,A2,Def8
.= (H2#(H1#x)).y by A1,A2,Def8;
end;
hence (H2**H1)#x = H2#(H1#x) by A1,FUNCT_1:9;
end;
definition let S; let U1,U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
pred F is_homomorphism U1,U2 means :Def9:
for o be OperSymbol of S st Args(o,U1) <> {}
for x be Element of Args(o,U1) holds
(F.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,U2).(F#x);
end;
theorem Th9:
for U1 being MSAlgebra over S holds
id (the Sorts of U1) is_homomorphism U1,U1
proof let U1 be MSAlgebra over S;
set F = id (the Sorts of U1);
let o be OperSymbol of S;
assume A1: Args(o,U1) <> {};
let x be Element of Args(o,U1);
set r = the_result_sort_of o;
A2: F#x = x by A1,Th7;
A3: F.r = id ((the Sorts of U1).r) by Def1;
A4: Result(o,U1) = ((the Sorts of U1)*(the ResultSort of S)).o
by MSUALG_1:def 10;
rng (the ResultSort of S) c= the carrier of S by RELSET_1:12;
then rng (the ResultSort of S) c= dom (the Sorts of U1) by PBOOLE:def 3;
then A5: dom ((the Sorts of U1)*(the ResultSort of S)) = dom (the ResultSort
of S)
by RELAT_1:46;
the OperSymbols of S <> {} by MSUALG_1:def 5;
then o in the OperSymbols of S;
then o in dom (the ResultSort of S) by FUNCT_2:def 1;
then A6: Result(o,U1) = (the Sorts of U1).((the ResultSort of S).o)
by A4,A5,FUNCT_1:22
.= (the Sorts of U1).r by MSUALG_1:def 7;
per cases; suppose Result(o,U1) <> {};
then A7: dom Den(o,U1) = Args(o,U1) & rng Den(o,U1) c= Result(o,U1)
by FUNCT_2:def 1,RELSET_1:12;
then Den(o,U1).x in rng Den(o,U1) by A1,FUNCT_1:def 5;
hence (F.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,U1).(F#x)
by A2,A3,A6,A7,FUNCT_1:35;
suppose Result(o,U1) = {};
then dom Den(o,U1) = {} & dom (F.r) = {} by A1,A6,FUNCT_2:def 1,RELAT_1:60;
then Den(o,U1).x = {} & (F.r).{} = {} by FUNCT_1:def 4;
hence thesis by A1,Th7;
end;
theorem Th10:
for U1,U2,U3 being non-empty MSAlgebra over S
for H1 be ManySortedFunction of U1,U2, H2 be ManySortedFunction of U2,U3 st
H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds
H2 ** H1 is_homomorphism U1,U3
proof let U1,U2,U3 be non-empty MSAlgebra over S;
let H1 be ManySortedFunction of U1,U2,H2 be ManySortedFunction of U2,U3;
assume A1: H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3;
let o be OperSymbol of S such that Args(o,U1) <> {};
let x be Element of Args(o,U1);
set F = H2**H1,
r = the_result_sort_of o;
(H1.r).(Den(o,U1).x) = Den(o,U2).(H1#x) by A1,Def9;
then A2: (H2.r).((H1.r).(Den(o,U1).x)) = Den(o,U3).(H2#(H1#x)) by A1,Def9;
A3: F.r = (H2.r)*(H1.r) by Th2;
A4: dom (F.r) = (the Sorts of U1).r by FUNCT_2:def 1;
A5: Result(o,U1) = ((the Sorts of U1)*(the ResultSort of S)).o
by MSUALG_1:def 10;
rng (the ResultSort of S) c= the carrier of S by RELSET_1:12;
then rng (the ResultSort of S) c= dom (the Sorts of U1) by PBOOLE:def 3;
then A6: dom ((the Sorts of U1)*(the ResultSort of S)) =
dom (the ResultSort of S) by RELAT_1:46;
the OperSymbols of S <> {} by MSUALG_1:def 5;
then o in the OperSymbols of S;
then o in dom (the ResultSort of S) by FUNCT_2:def 1;
then Result(o,U1) = (the Sorts of U1).((the ResultSort of S).o)
by A5,A6,FUNCT_1:22
.= (the Sorts of U1).r by MSUALG_1:def 7;
then (F.r).(Den(o,U1).x) = Den(o,U3).(H2#(H1#x)) by A2,A3,A4,FUNCT_1:22;
hence (F.r).(Den(o,U1).x) = Den(o,U3).(F#x) by Th8;
end;
definition let S; let U1,U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
pred F is_epimorphism U1,U2 means :Def10:
F is_homomorphism U1,U2 & F is "onto";
end;
theorem Th11:
for U1,U2,U3 being non-empty MSAlgebra over S
for F be ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3 st
F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G**F is_epimorphism U1,U3
proof let U1,U2,U3 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2,
G be ManySortedFunction of U2,U3;
assume F is_epimorphism U1,U2 & G is_epimorphism U2,U3;
then A1: F is_homomorphism U1,U2 & F is "onto" &
G is_homomorphism U2,U3 & G is "onto" by Def10;
then A2: G**F is_homomorphism U1,U3 by Th10;
for i be set st i in (the carrier of S)
holds rng((G**F).i) = (the Sorts of U3).i
proof
let i be set;
assume A3: i in the carrier of S;
then reconsider f = F.i as Function of (the Sorts of U1).i,(the Sorts of
U2).i
by MSUALG_1:def 2;
reconsider g = G.i as Function of (the Sorts of U2).i,(the Sorts of U3).i
by A3,MSUALG_1:def 2;
A4: rng f = (the Sorts of U2).i by A1,A3,Def3;
A5: rng g = (the Sorts of U3).i by A1,A3,Def3;
(the Sorts of U3).i = {} implies (the Sorts of U2).i = {}
by A3,PBOOLE:def 16;
then dom g = rng f by A4,FUNCT_2:def 1;
then rng (g*f) = (the Sorts of U3).i by A5,RELAT_1:47;
hence thesis by A3,Th2;
end;
then G**F is "onto" by Def3;
hence thesis by A2,Def10;
end;
definition let S; let U1,U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
pred F is_monomorphism U1,U2 means :Def11:
F is_homomorphism U1,U2 & F is "1-1";
end;
theorem Th12:
for U1,U2,U3 being non-empty MSAlgebra over S
for F be ManySortedFunction of U1,U2, G be ManySortedFunction of U2,U3 st
F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds
G**F is_monomorphism U1,U3
proof let U1,U2,U3 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2,
G be ManySortedFunction of U2,U3;
assume F is_monomorphism U1,U2 & G is_monomorphism U2,U3;
then A1: F is_homomorphism U1,U2 & F is "1-1" &
G is_homomorphism U2,U3 & G is "1-1" by Def11;
then A2: G**F is_homomorphism U1,U3 by Th10;
for i be set, h be Function st i in dom (G**F) & (G**F).i = h holds
h is one-to-one
proof
let i be set,h be Function;
assume A3: i in dom (G**F) & (G**F).i = h;
then A4: i in the carrier of S by PBOOLE:def 3;
then A5: i in dom F by PBOOLE:def 3;
A6: i in dom G by A4,PBOOLE:def 3;
reconsider f = F.i as Function of (the Sorts of U1).i,(the Sorts of U2).i
by A4,MSUALG_1:def 2;
reconsider g = G.i as Function of (the Sorts of U2).i,(the Sorts of U3).i
by A4,MSUALG_1:def 2;
A7: f is one-to-one by A1,A5,Def2;
g is one-to-one by A1,A6,Def2;
then g*f is one-to-one by A7,FUNCT_1:46;
hence thesis by A3,A4,Th2;
end;
then G**F is "1-1" by Def2;
hence thesis by A2,Def11;
end;
definition let S; let U1,U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
pred F is_isomorphism U1,U2 means :Def12:
F is_epimorphism U1,U2 & F is_monomorphism U1,U2;
end;
theorem Th13:
for F be ManySortedFunction of U1,U2 holds
F is_isomorphism U1,U2 iff
F is_homomorphism U1,U2 & F is "onto" & F is "1-1"
proof
let F be ManySortedFunction of U1,U2;
thus F is_isomorphism U1,U2 implies F is_homomorphism U1,U2 &
F is "onto" & F is "1-1"
proof
assume F is_isomorphism U1,U2;
then F is_epimorphism U1,U2 & F is_monomorphism U1,U2 by Def12;
hence thesis by Def10,Def11;
end;
assume A1: F is_homomorphism U1,U2 & F is "onto" & F is "1-1";
then A2: F is_epimorphism U1,U2 by Def10;
F is_monomorphism U1,U2 by A1,Def11;
hence thesis by A2,Def12;
end;
Lm3:
for U1,U2 being non-empty MSAlgebra over S
for H be ManySortedFunction of U1,U2 st
H is_isomorphism U1,U2 holds H"" is_homomorphism U2,U1
proof let U1,U2 be non-empty MSAlgebra over S;
let H be ManySortedFunction of U1,U2;
assume A1: H is_isomorphism U1,U2;
set F = H"";
A2: H is_homomorphism U1,U2 & H is "onto" & H is "1-1" by A1,Th13;
for o be OperSymbol of S st Args(o,U2) <> {}
for x be Element of Args(o,U2) holds
(F.(the_result_sort_of o)).(Den(o,U2).x) = Den(o,U1).(F#x)
proof
let o be OperSymbol of S such that Args(o,U2) <> {};
let x be Element of Args(o,U2);
set r = the_result_sort_of o;
deffunc G(set)=(F#x).$1;
consider f being Function such that A3: dom f = dom (the_arity_of o) &
for n be set st n in dom (the_arity_of o) holds f.n = G(n)
from Lambda;
A4: dom (F#x) = dom (the_arity_of o) by Th6;
then A5: f = (F#x) by A3,FUNCT_1:9;
reconsider f as Element of Args(o,U1) by A3,A4,FUNCT_1:9;
r in the carrier of S;
then A6: r in dom H by PBOOLE:def 3;
A7: dom (H.r) = (the Sorts of U1).r & rng (H.r) c= (the Sorts of U2).r
by FUNCT_2:def 1,RELSET_1:12;
A8: dom ((F.r)*(H.r)) = (the Sorts of U1).r by FUNCT_2:def 1;
A9: the OperSymbols of S <> {} by MSUALG_1:def 5;
A10: dom (the ResultSort of S) = the OperSymbols of S &
rng (the ResultSort of S) c= the carrier of S
by FUNCT_2:def 1,RELSET_1:12;
then A11: dom ((the Sorts of U1)*(the ResultSort of S)) =
dom (the ResultSort of S) by PBOOLE:def 3;
A12: Result(o,U1) = ((the Sorts of U1)*(the ResultSort of S)).o
by MSUALG_1:def 10
.= (the Sorts of U1).((the ResultSort of S).o) by A9,A10,A11,FUNCT_1
:22
.= (the Sorts of U1).r by MSUALG_1:def 7;
A13: F.r = (H.r)" by A2,Def5;
H.r is one-to-one by A2,A6,Def2;
then A14: (F.r)*(H.r) = id ((the Sorts of U1).r) by A7,A13,FUNCT_1:61;
(H.r).(Den(o,U1).f) = Den(o,U2).(H#(F#x)) by A2,A5,Def9
.= Den(o,U2).((H**F)#x) by Th8
.= Den(o,U2).((id (the Sorts of U2))#x) by A2,Th5
.= Den(o,U2).x by Th7;
then (F.r).(Den(o,U2).x) = ((F.r)*(H.r)).(Den(o,U1).(F#x)) by A5,A8,A12,
FUNCT_1:22
.= Den(o,U1).(F#x) by A12,A14,FUNCT_1:35;
hence thesis;
end;
hence thesis by Def9;
end;
theorem Th14:
for U1,U2 being non-empty MSAlgebra over S
for H be ManySortedFunction of U1,U2, H1 be ManySortedFunction of U2,U1 st
H is_isomorphism U1,U2 & H1 = H"" holds H1 is_isomorphism U2,U1
proof let U1,U2 be non-empty MSAlgebra over S;
let H be ManySortedFunction of U1,U2,H1 be ManySortedFunction of U2,U1;
assume A1: H is_isomorphism U1,U2 & H1 = H"";
then A2: H is_monomorphism U1,U2 & H is_epimorphism U1,U2 by Def12;
then A3: H is_homomorphism U1,U2 & H is "1-1" by Def11;
A4: H is "onto" by A2,Def10;
A5: for i be set, g be Function st i in dom H1 &
g = H1.i holds g is one-to-one
proof
let i be set;
let g be Function;
assume A6: i in dom H1 & g = H1.i;
then A7: i in the carrier of S by PBOOLE:def 3;
then A8: i in dom H by PBOOLE:def 3;
reconsider f = H.i as Function of (the Sorts of U1).i,(the Sorts of U2).i
by A7,MSUALG_1:def 2;
f is one-to-one by A3,A8,Def2;
then f" is one-to-one by FUNCT_1:62;
hence thesis by A1,A3,A4,A6,A7,Def5;
end;
for i be set st i in
(the carrier of S) holds rng(H1.i) = (the Sorts of U1).i
proof
let i be set;
assume A9: i in (the carrier of S);
then A10: i in dom H by PBOOLE:def 3;
reconsider f = H.i as Function of (the Sorts of U1).i,(the Sorts of U2).i
by A9,MSUALG_1:def 2;
f is one-to-one by A3,A10,Def2;
then A11: rng (f") = dom f by FUNCT_1:55;
(the Sorts of U2).i = {} implies (the Sorts of U1).i = {}
by A9,PBOOLE:def 16;
then rng (f") = (the Sorts of U1).i by A11,FUNCT_2:def 1;
hence thesis by A1,A3,A4,A9,Def5;
end;
then A12: H1 is "onto" by Def3;
A13: H1 is "1-1" by A5,Def2;
A14: H1 is_homomorphism U2,U1 by A1,Lm3;
then A15: H1 is_epimorphism U2,U1 by A12,Def10;
H1 is_monomorphism U2,U1 by A13,A14,Def11;
hence thesis by A15,Def12;
end;
theorem Th15:
for U1,U2,U3 being non-empty MSAlgebra over S
for H be ManySortedFunction of U1,U2, H1 be ManySortedFunction of U2,U3 st
H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3
holds H1 ** H is_isomorphism U1,U3
proof let U1,U2,U3 be non-empty MSAlgebra over S;
let H be ManySortedFunction of U1,U2,H1 be ManySortedFunction of U2,U3;
assume A1: H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3;
then A2: H is_epimorphism U1,U2 & H is_monomorphism U1,U2 by Def12;
A3: H1 is_monomorphism U2,U3 & H1 is_epimorphism U2,U3 by A1,Def12;
then A4: H1**H is_epimorphism U1,U3 by A2,Th11;
H1**H is_monomorphism U1,U3 by A2,A3,Th12;
hence thesis by A4,Def12;
end;
definition let S; let U1,U2 be MSAlgebra over S;
pred U1,U2 are_isomorphic means :Def13:
ex F be ManySortedFunction of U1,U2 st F is_isomorphism U1,U2;
end;
theorem Th16:
for U1 being MSAlgebra over S holds
id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic
proof let U1 be MSAlgebra over S;
A1: id (the Sorts of U1) is_homomorphism U1,U1 by Th9;
A2: for i be set,f be Function st i in dom id (the Sorts of U1) &
(id (the Sorts of U1)).i = f holds f is one-to-one
proof
let i be set,f be Function;
assume A3: i in dom id (the Sorts of U1) & (id (the Sorts of U1)).i = f;
then i in the carrier of S by PBOOLE:def 3;
then f = id ((the Sorts of U1).i) by A3,Def1;
hence f is one-to-one;
end;
for i be set st i in (the carrier of S)
holds rng((id (the Sorts of U1)).i) = (the Sorts of U1).i
proof
let i be set;
assume i in (the carrier of S);
then (id (the Sorts of U1)).i = id ((the Sorts of U1).i) by Def1;
hence thesis by RELAT_1:71;
end;
then A4: id (the Sorts of U1) is "onto" by Def3;
id (the Sorts of U1) is "1-1" by A2,Def2;
then A5: id (the Sorts of U1) is_monomorphism U1,U1 by A1,Def11;
A6: id (the Sorts of U1) is_epimorphism U1,U1 by A1,A4,Def10;
hence id (the Sorts of U1) is_isomorphism U1,U1 by A5,Def12;
take id (the Sorts of U1);
thus thesis by A5,A6,Def12;
end;
definition let S; let U1, U2 be MSAlgebra over S;
redefine pred U1, U2 are_isomorphic;
reflexivity by Th16;
end;
theorem
for U1,U2 being non-empty MSAlgebra over S holds
U1,U2 are_isomorphic implies U2,U1 are_isomorphic
proof let U1,U2 be non-empty MSAlgebra over S;
assume U1,U2 are_isomorphic;
then consider F be ManySortedFunction of U1,U2 such that
A1: F is_isomorphism U1,U2 by Def13;
reconsider G = F"" as ManySortedFunction of U2,U1;
G is_isomorphism U2,U1 by A1,Th14;
hence thesis by Def13;
end;
theorem
for U1,U2,U3 being non-empty MSAlgebra over S holds
U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic
proof let U1,U2,U3 be non-empty MSAlgebra over S;
assume A1: U1,U2 are_isomorphic & U2,U3 are_isomorphic;
then consider F be ManySortedFunction of U1,U2 such that
A2: F is_isomorphism U1,U2 by Def13;
consider G be ManySortedFunction of U2,U3 such that
A3: G is_isomorphism U2,U3 by A1,Def13;
reconsider H = G**F as ManySortedFunction of U1,U3;
H is_isomorphism U1,U3 by A2,A3,Th15;
hence thesis by Def13;
end;
definition let S; let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2;
func Image F -> strict non-empty MSSubAlgebra of U2 means :Def14:
the Sorts of it = F.:.:(the Sorts of U1);
existence
proof
set u2 = F.:.:(the Sorts of U1);
u2 is non-empty MSSubset of U2
proof
now
let i be set; assume A2: i in the carrier of S;
reconsider f = F.i as Function;
A3: u2.i = f.:((the Sorts of U1).i) by A2,Def6;
reconsider f as Function of (the Sorts of U1).i,(the Sorts of U2).i
by A2,MSUALG_1:def 2;
(the Sorts of U2).i = {} implies (the Sorts of U1).i = {}
by A2,PBOOLE:def 16;
then dom f = (the Sorts of U1).i & rng f c= (the Sorts of U2).i
by FUNCT_2:def 1,RELSET_1:12;
hence u2.i c= (the Sorts of U2).i by A3,RELAT_1:146;
end;
then A4: u2 c= the Sorts of U2 by PBOOLE:def 5;
now
let i be set; assume A5: i in the carrier of S;
reconsider f = F.i as Function;
A6: u2.i = f.:((the Sorts of U1).i) by A5,Def6;
reconsider f as Function of (the Sorts of U1).i,(the Sorts of U2).i
by A5,MSUALG_1:def 2;
A7: (the Sorts of U1).i <> {} by A5,PBOOLE:def 16;
(the Sorts of U2).i = {} implies (the Sorts of U1).i = {}
by A5,PBOOLE:def 16;
then dom f = (the Sorts of U1).i by FUNCT_2:def 1;
hence u2.i is non empty by A6,A7,RELAT_1:152;
end;
hence u2 is non-empty MSSubset of U2 by A4,MSUALG_2:def 1,PBOOLE:def 16;
end;
then reconsider u2 as non-empty MSSubset of U2;
set M = GenMSAlg(u2);
reconsider M' = MSAlgebra (#u2 , Opers(U2,u2) qua ManySortedFunction of
(u2# * the Arity of S),(u2 * the ResultSort of S)#)
as non-empty MSAlgebra over S by MSUALG_1:def 8;
take M;
u2 is opers_closed
proof
let o be OperSymbol of S;
thus rng ((Den(o,U2))|((u2# * the Arity of S).o)) c=
(u2 * the ResultSort of S).o
proof
set D = Den(o,U2),
X = (u2# * the Arity of S).o,
ao = the_arity_of o,
ro = the_result_sort_of o,
ut = u2 * ao,
S1 = the Sorts of U1;
let x be set;
assume x in rng (D|X);
then consider a be set such that A8: a in
dom(D|X) & x = (D|X).a by FUNCT_1:def 5;
A9: dom (D|X) c= X by RELAT_1:87;
A10: dom (D|X) c= dom D by FUNCT_1:76;
A11: x = D.a by A8,FUNCT_1:70;
reconsider a as Element of Args(o,U2) by A8,A10,FUNCT_2:def 1;
A12: dom (the Arity of S) = the OperSymbols of S &
rng (the Arity of S) c= (the carrier of S)*
by FUNCT_2:def 1,RELSET_1:12;
then A13: dom (u2# * (the Arity of S)) = dom (the Arity of S) by PBOOLE:
def 3;
A14: the OperSymbols of S <> {} by MSUALG_1:def 5;
then X = u2#.((the Arity of S).o) by A12,A13,FUNCT_1:22
.= u2#.(ao) by MSUALG_1:def 6
.= product(u2 * ao) by MSUALG_1:def 3;
then A15: dom a = dom ut &
for y be set st y in dom ut holds (a).y in ut.y by A8,A9,CARD_3:18;
A16: dom u2 = the carrier of S by PBOOLE:def 3;
A17: rng ao c= the carrier of S by FINSEQ_1:def 4;
defpred P[set,set] means
for s be SortSymbol of S st s = ao.$1 holds $2 in S1.s & (a).$1=(F.s).$2;
A18: for y be set st y in dom (a) ex i be set st P[y,i]
proof
let y be set; assume A19: y in dom (a);
dom (u2 * ao) = dom ao by A16,A17,RELAT_1:46;
then ao.y in rng ao by A15,A19,FUNCT_1:def 5;
then reconsider s = ao.y as SortSymbol of S by A17;
A20: dom (F.s) = S1.s & rng (F.s) c= (the Sorts of U2).s
by FUNCT_2:def 1,RELSET_1:12;
A21: a.y in ut.y by A15,A19;
ut.y = u2.(ao.y) by A15,A19,FUNCT_1:22
.= (F.s).:(S1.s) by Def6
.= rng (F.s) by A20,RELAT_1:146;
then consider i be set such that A22: i in S1.s & (a).y = (F.s).i
by A20,A21,FUNCT_1:def 5;
take i;
thus thesis by A22;
end;
consider f be Function such that
A23: dom f = dom a &
for y be set st y in dom a holds P[y,f.y] from NonUniqFuncEx(A18);
A24: Args(o,U1) = product (S1 * ao) by PRALG_2:10;
A25: dom f = dom ao by A15,A16,A17,A23,RELAT_1:46;
dom S1 = the carrier of S by PBOOLE:def 3;
then A26: dom (S1 * ao) = dom ao by A17,RELAT_1:46;
for y be set st y in dom(S1 * ao) holds f.y in (S1 * ao).y
proof
let y be set; assume A27: y in dom (S1 * ao);
then ao.y in rng ao by A26,FUNCT_1:def 5;
then reconsider s = ao.y as SortSymbol of S by A17;
f.y in S1.s by A23,A25,A26,A27; hence thesis by A27,FUNCT_1:22;
end;
then reconsider a1 = f as Element of Args(o,U1) by A24,A25,A26,CARD_3:18;
A28: dom (F#a1) = dom ao & dom a1 = dom ao &
dom a = dom ao by Th6;
now
let y be set;
assume A29: y in dom ao;
then reconsider n = y as Nat;
ao.y in rng ao by A29,FUNCT_1:def 5;
then reconsider s = ao.y as SortSymbol of S by A17;
(F#a1).n = (F.(ao/.n)).(a1.n) by A28,A29,Def8
.= (F.s).(a1.n) by A29,FINSEQ_4:def 4;
hence (F#a1).y = a.y by A23,A28,A29;
end;
then F#a1 = a by A28,FUNCT_1:9;
then A30: (F.ro).(Den(o,U1).a1) = x by A1,A11,Def9;
A31: dom (the ResultSort of S) = the OperSymbols of S &
rng (the ResultSort of S) c= the carrier of S
by FUNCT_2:def 1,RELSET_1:12;
then A32: dom (S1 * (the ResultSort of S)) = dom (the ResultSort of S)
by PBOOLE:def 3;
Result(o,U1) = (S1 * (the ResultSort of S)).o by MSUALG_1:def 10
.= S1.((the ResultSort of S).o) by A14,A31,A32,FUNCT_1:22
.= S1.ro by MSUALG_1:def 7;
then A33: Den(o,U1).a1 in S1.ro;
A34: dom (F.ro) = S1.ro by FUNCT_2:def 1;
A35: Den(o,U1).a1 in dom (F.ro) by A33,FUNCT_2:def 1;
reconsider g = F.ro as Function;
dom (u2 * the ResultSort of S) = dom (the ResultSort of S)
by A31,PBOOLE:def 3;
then (u2 * the ResultSort of S).o = u2.((the ResultSort of S).o)
by A14,A31,FUNCT_1:22
.= u2.ro by MSUALG_1:def 7
.= g.:(S1.ro) by Def6
.= rng g by A34,RELAT_1:146;
hence thesis by A30,A35,FUNCT_1:def 5;
end;
end;
then for B be MSSubset of U2 st B = the Sorts of M' holds
B is opers_closed & the Charact of M' = Opers(U2,B);
then M' is MSSubAlgebra of U2 & u2 is MSSubset of M'
by MSUALG_2:def 1,def 10;
then M is MSSubAlgebra of M' by MSUALG_2:def 18;
then the Sorts of M is MSSubset of M' & u2 is MSSubset of M
by MSUALG_2:def 10,def 18;
then the Sorts of M c= u2 & u2 c= the Sorts of M by MSUALG_2:def 1;
hence thesis by PBOOLE:def 13;
end;
uniqueness by MSUALG_2:10;
end;
theorem
for U1 being non-empty MSAlgebra over S,
U2 being strict non-empty MSAlgebra over S,
F be ManySortedFunction of U1,U2
st F is_homomorphism U1,U2 holds F is_epimorphism U1,U2 iff Image F = U2
proof let U1 be non-empty MSAlgebra over S;
let U2 be strict non-empty MSAlgebra over S,
F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2;
set FF = F.:.:(the Sorts of U1);
thus F is_epimorphism U1,U2 implies Image F = U2
proof
assume F is_epimorphism U1,U2;
then A2: F is "onto" by Def10;
now
let i be set; assume A3: i in the carrier of S;
then reconsider f = F.i as
Function of (the Sorts of U1).i,(the Sorts of U2).i by MSUALG_1:def 2;
A4: rng f = (the Sorts of U2).i by A2,A3,Def3;
reconsider f as Function;
A5: FF.i = f.:((the Sorts of U1).i) by A3,Def6;
(the Sorts of U2).i = {} implies (the Sorts of U1).i = {}
by A3,PBOOLE:def 16;
then dom f = (the Sorts of U1).i by FUNCT_2:def 1;
hence FF.i = (the Sorts of U2).i by A4,A5,RELAT_1:146;
end;
then A6: FF = the Sorts of U2 by PBOOLE:3;
U2 is strict MSSubAlgebra of U2 by MSUALG_2:6;
hence thesis by A1,A6,Def14;
end;
assume Image F = U2;
then A7: FF = the Sorts of U2 by A1,Def14;
for i be set st i in the carrier of S holds rng(F.i) = (the Sorts of U2).i
proof
let i be set;
assume i in the carrier of S;
then reconsider i as Element of S;
reconsider f = F.i as
Function of (the Sorts of U1).i,(the Sorts of U2).i;
A8: f.:((the Sorts of U1).i) = (the Sorts of U2).i by A7,Def6;
dom f = (the Sorts of U1).i by FUNCT_2:def 1;
hence thesis by A8,RELAT_1:146;
end;
then F is "onto" by Def3;
hence thesis by A1,Def10;
end;
Lm4:
for U1,U2 being non-empty MSAlgebra over S
for F be ManySortedFunction of U1,U2 st F is_homomorphism U1,U2
holds F is ManySortedFunction of U1,Image F
proof let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2;
for i be set st i in the carrier of S holds
F.i is Function of (the Sorts of U1).i,(the Sorts of Image F).i
proof
let i be set;
assume A2: i in the carrier of S;
then reconsider f = F.i as
Function of (the Sorts of U1).i,(the Sorts of U2).i by MSUALG_1:def 2;
(the Sorts of U2).i = {} implies (the Sorts of U1).i = {}
by A2,PBOOLE:def 16;
then A3: dom f = (the Sorts of U1).i & rng f c= (the Sorts of U2).i
by FUNCT_2:def 1,RELSET_1:12;
the Sorts of Image F = F.:.:(the Sorts of U1) by A1,Def14;
then (the Sorts of Image F).i = f.:((the Sorts of U1).i) by A2,Def6
.= rng f by A3,RELAT_1:146; hence thesis by A3,
FUNCT_2:3;
end;
hence thesis by MSUALG_1:def 2;
end;
theorem Th20:
for U1,U2 being non-empty MSAlgebra over S
for F be ManySortedFunction of U1,U2, G be ManySortedFunction of U1,Image F
st F = G & F is_homomorphism U1,U2 holds G is_epimorphism U1,Image F
proof let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2,
G be ManySortedFunction of U1,Image F;
assume A1: F = G & F is_homomorphism U1,U2;
for o be OperSymbol of S st Args(o,U1) <> {}
for x be Element of Args(o,U1) holds
(G.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,Image F).(G#x)
proof
let o be OperSymbol of S such that Args(o,U1) <> {};
let x be Element of Args(o,U1);
reconsider G1 = G as ManySortedFunction of U1,U2 by A1;
A2: dom (G#x) = dom (the_arity_of o) &
dom (G1#x) = dom (the_arity_of o) by Th6;
A3: dom x = dom (the_arity_of o) by Th6;
now
let a be set;
assume A4: a in dom (the_arity_of o);
then reconsider n = a as Nat;
(G#x).n = (G.((the_arity_of o)/.n)).(x.n) &
(G1#x).n = (G1.((the_arity_of o)/.n)).(x.n) by A3,A4,Def8;
hence (G#x).a = (G1#x).a;
end;
then G#x = G1#x by A2,FUNCT_1:9;
then A5: (G.(the_result_sort_of o)).(Den(o,U1).x)= Den(o,U2).(G#x) by A1,
Def9;
set IF = Image F;
reconsider SIF = the Sorts of IF as non-empty MSSubset of U2
by MSUALG_2:def 10;
A6: the Charact of IF = Opers(U2,SIF) & SIF is opers_closed
by MSUALG_2:def 10;
then A7: SIF is_closed_on o by MSUALG_2:def 7;
A8: Den(o,IF) = (Opers(U2,SIF)).o by A6,MSUALG_1:def 11
.= o/.(SIF) by MSUALG_2:def 9
.= (Den(o,U2))|((SIF# * the Arity of S).o)
by A7,MSUALG_2:def 8;
A9:(SIF# * the Arity of S).o = Args(o,IF) by MSUALG_1:def 9;
set SIF_o = SIF * (the_arity_of o),
Uo = (the Sorts of U2) * (the_arity_of o),
ao = the_arity_of o;
A10: Args(o,IF) = product(SIF_o) by PRALG_2:10;
A11: Args(o,U2) = product(Uo) by PRALG_2:10;
A12: rng ao c= the carrier of S by FINSEQ_1:def 4;
then rng ao c= dom SIF by PBOOLE:def 3;
then A13: dom SIF_o = dom ao by RELAT_1:46;
rng ao c= dom (the Sorts of U2) by A12,PBOOLE:def 3;
then A14: dom SIF_o = dom Uo by A13,RELAT_1:46;
for x be set st x in dom SIF_o holds SIF_o.x c= Uo.x
proof
let x be set;
assume A15: x in dom SIF_o;
then ao.x in rng ao by A13,FUNCT_1:def 5;
then reconsider k = ao.x as Element of S by A12;
set f = F.k;
A16: dom f = (the Sorts of U1).k & rng f c= (the Sorts of U2).k
by FUNCT_2:def 1,RELSET_1:12;
SIF = F.:.:(the Sorts of U1) by A1,Def14;
then SIF_o.x = (F.:.:(the Sorts of U1)).k by A15,FUNCT_1:22
.= f.:((the Sorts of U1).k) by Def6
.= rng f by A16,RELAT_1:146; hence thesis by A14,A15,A16,FUNCT_1
:22;
end;
then A17: Args(o,IF) c= Args(o,U2) by A10,A11,A14,CARD_3:38;
dom Den(o,U2) = Args(o,U2) by FUNCT_2:def 1;
then G#x in (SIF# * the Arity of S).o & G#x in dom Den(o,U2)
by A9,A17,TARSKI:def 3;
then G#x in (dom Den(o,U2)) /\ Args(o,IF) by XBOOLE_0:def 3
; hence thesis by A5,A8,A9,FUNCT_1:71;
end;
then A18: G is_homomorphism U1,Image F by Def9;
for i be set st i in the carrier of S
holds rng(G.i) = (the Sorts of Image F).i
proof
let i be set;
assume i in the carrier of S;
then reconsider i as Element of S;
set g = G.i;
the Sorts of (Image F) = G.:.:(the Sorts of U1) by A1,Def14;
then A19: (the Sorts of Image F).i = g.:((the Sorts of U1).i) by Def6;
dom g = (the Sorts of U1).i by FUNCT_2:def 1; hence thesis by A19,
RELAT_1:146;
end;
then G is "onto" by Def3;
hence thesis by A18,Def10;
end;
theorem
for U1,U2 being non-empty MSAlgebra over S
for F be ManySortedFunction of U1,U2 st F is_homomorphism U1,U2
ex G be ManySortedFunction of U1,Image F
st F = G & G is_epimorphism U1,Image F
proof let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2;
then reconsider G = F as ManySortedFunction of U1,Image F by Lm4;
take G;
thus thesis by A1,Th20;
end;
Lm5:
for U1,U2 being non-empty MSAlgebra over S
for U3 be non-empty MSSubAlgebra of U2, F be ManySortedFunction of U1,U2,
G be ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds
F is_homomorphism U1,U2
proof let U1,U2 be non-empty MSAlgebra over S;
let U3 be non-empty MSSubAlgebra of U2,
F be ManySortedFunction of U1,U2,
G be ManySortedFunction of U1,U3;
assume A1: F = G & G is_homomorphism U1,U3;
for o be OperSymbol of S st Args(o,U1) <> {}
for x be Element of Args(o,U1) holds
(F.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,U2).(F#x)
proof
let o be OperSymbol of S such that Args(o,U1) <> {};
let x be Element of Args(o,U1);
for i be set st i in the carrier of S holds
G.i is Function of (the Sorts of U1).i, (the Sorts of U2).i
proof
let i be set;
assume A2: i in the carrier of S;
then reconsider g = G.i as
Function of (the Sorts of U1).i,(the Sorts of U3).i
by MSUALG_1:def 2;
A3: (the Sorts of U3).i = {} implies (the Sorts of U1).i = {}
by A2,PBOOLE:def 16;
reconsider S3 = the Sorts of U3 as non-empty MSSubset of U2
by MSUALG_2:def 10;
the Sorts of U3 is MSSubset of U2 by MSUALG_2:def 10;
then the Sorts of U3 c= the Sorts of U2 by MSUALG_2:def 1;
then S3.i c= (the Sorts of U2).i by A2,PBOOLE:def 5;
then g is Function of (the Sorts of U1).i,(the Sorts of U2).i
by A3,FUNCT_2:9;
hence thesis;
end;
then reconsider G1 = G as ManySortedFunction of U1,U2 by MSUALG_1:def 2;
A4: dom (G#x) = dom (the_arity_of o) &
dom (G1#x) = dom (the_arity_of o) &
dom (F#x) = dom (the_arity_of o) by Th6;
A5: dom x = dom (the_arity_of o) by Th6;
now
let a be set;
assume A6: a in dom (the_arity_of o);
then reconsider n = a as Nat;
(G#x).n = (G.((the_arity_of o)/.n)).(x.n) &
(G1#x).n = (G1.((the_arity_of o)/.n)).(x.n) by A5,A6,Def8;
hence (G#x).a = (G1#x).a;
end;
then A7: G#x = G1#x by A4,FUNCT_1:9;
then A8: (F.(the_result_sort_of o)).(Den(o,U1).x)= Den(o,U3).(F#x) by A1,
Def9;
reconsider S3 = the Sorts of U3 as non-empty MSSubset of U2
by MSUALG_2:def 10;
A9: the Charact of U3 = Opers(U2,S3) & S3 is opers_closed
by MSUALG_2:def 10;
then A10: S3 is_closed_on o by MSUALG_2:def 7;
A11: Den(o,U3) = (Opers(U2,S3)).o by A9,MSUALG_1:def 11
.= o/.(S3) by MSUALG_2:def 9
.= (Den(o,U2))|((S3# * the Arity of S).o)
by A10,MSUALG_2:def 8;
A12:(S3# * the Arity of S).o = Args(o,U3) by MSUALG_1:def 9;
dom Den(o,U2) = Args(o,U2) by FUNCT_2:def 1;
then F#x in (dom Den(o,U2)) /\ Args(o,U3) by A1,A7,XBOOLE_0:def 3;
hence thesis by A8,A11,A12,FUNCT_1:71;
end;
hence thesis by Def9;
end;
theorem Th22:
for U1 being non-empty MSAlgebra over S
for U2 be non-empty MSSubAlgebra of U1,
G be ManySortedFunction of U2,U1 st
G = id (the Sorts of U2) holds G is_monomorphism U2,U1
proof let U1 be non-empty MSAlgebra over S;
let U2 be non-empty MSSubAlgebra of U1,
G be ManySortedFunction of U2,U1;
assume A1: G =id (the Sorts of U2);
set F = id (the Sorts of U2);
F is_homomorphism U2,U2 by Th9;
then A2: G is_homomorphism U2,U1 by A1,Lm5;
for i be set st i in the carrier of S holds G.i is one-to-one
proof
let i be set;
assume A3: i in the carrier of S;
then reconsider f = F.i as Function of (the Sorts of U2).i,(the Sorts of U2
).i
by MSUALG_1:def 2;
f = id ((the Sorts of U2).i) by A3,Def1; hence thesis by A1;
end;
then G is "1-1" by Th1;
hence thesis by A2,Def11;
end;
theorem
for U1,U2 being non-empty MSAlgebra over S
for F be ManySortedFunction of U1,U2 st F is_homomorphism U1,U2
ex F1 be ManySortedFunction of U1,Image F,
F2 be ManySortedFunction of Image F,U2 st
F1 is_epimorphism U1,Image F & F2 is_monomorphism Image F,U2 &
F = F2**F1
proof let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2;
then reconsider F1 = F as ManySortedFunction of U1,Image F by Lm4;
for H be ManySortedFunction of Image F,Image F
holds H is ManySortedFunction of Image F,U2
proof
let H be ManySortedFunction of Image F,Image F;
for i be set st i in the carrier of S holds
H.i is Function of (the Sorts of Image F).i,(the Sorts of U2).i
proof
let i be set;
assume A2: i in the carrier of S;
then reconsider h = H.i as
Function of (the Sorts of Image F).i,(the Sorts of Image F).i
by MSUALG_1:def 2;
reconsider f = F.i as
Function of (the Sorts of U1).i,(the Sorts of U2).i
by A2,MSUALG_1:def 2;
(the Sorts of U2).i = {} implies (the Sorts of U1).i = {}
by A2,PBOOLE:def 16;
then A3: dom f = (the Sorts of U1).i & rng f c= (the Sorts of U2).i
by FUNCT_2:def 1,RELSET_1:12;
A4: (the Sorts of Image F).i = {} implies (the Sorts of Image F).i = {};
the Sorts of Image F = F.:.:(the Sorts of U1) by A1,Def14;
then (the Sorts of Image F).i = f.:((the Sorts of U1).i) by A2,Def6
.= rng f by A3,RELAT_1:146;
then h is Function of (the Sorts of Image F).i,(the Sorts of U2).i
by A3,A4,FUNCT_2:9;
hence thesis;
end;
hence thesis by MSUALG_1:def 2;
end;
then reconsider F2 = id (the Sorts of Image F) as
ManySortedFunction of Image F,U2;
take F1,F2;
thus F1 is_epimorphism U1,Image F by A1,Th20;
thus F2 is_monomorphism Image F,U2 by Th22;
thus F = F2**F1 by Th4;
end;
theorem
for S for U1,U2 being MSAlgebra over S for o
for F being ManySortedFunction of U1,U2
for x being Element of Args(o,U1), f,u being Function
st x = f & x in Args(o,U1) & u in Args(o,U2)
holds u = F#x iff
for n st n in dom f holds u.n = (F.((the_arity_of o)/.n)).(f.n) by Lm2;