:: More on Products of Many Sorted Algebras
:: by Mariusz Giero
::
:: Received April 29, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, PBOOLE, STRUCT_0, MSUALG_1, SUBSET_1, PRALG_2, EQREL_1,
FUNCT_1, CARD_3, RELAT_1, SETFAM_1, RLVECT_2, FUNCT_6, TARSKI, FUNCT_2,
MARGREL1, UNIALG_2, FUNCT_5, FUNCOP_1, FINSEQ_4, PARTFUN1, MSUALG_3,
MEMBER_1, ARYTM_3, WELLORD1, PRALG_3;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, STRUCT_0, FUNCT_2, FUNCOP_1, EQREL_1, FUNCT_5, FUNCT_6, CARD_3,
PBOOLE, MSUALG_1, MSUALG_3, PRALG_2, PRALG_1, MSUALG_2;
constructors EQREL_1, PRALG_1, PRALG_2, MSUALG_3, RELSET_1, FUNCT_5;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCOP_1, EQREL_1, PBOOLE, STRUCT_0, MSUALG_1, PRALG_2, MSUALG_3, CARD_3,
RELSET_1;
requirements BOOLE, SUBSET;
definitions XBOOLE_0, FUNCT_1, MSUALG_3, PRALG_2, PBOOLE, TARSKI;
equalities PRALG_2;
expansions XBOOLE_0, FUNCT_1, MSUALG_3, PBOOLE, TARSKI;
theorems PBOOLE, FUNCT_1, EQREL_1, PRALG_2, MSUALG_1, MSUALG_3, FUNCT_2,
CARD_3, TARSKI, FUNCOP_1, MSUALG_2, PRALG_1, FUNCT_6, RELAT_1, RELSET_1,
XBOOLE_0, XBOOLE_1, PARTFUN1, MSUALG_6;
schemes PBOOLE, MSSUBFAM;
begin ::Preliminaries
::-------------------------------------------------------------------
:: Acknowledgements:
:: ================
::
:: I would like to thank Professor A.Trybulec for his help in the preparation
:: of the article.
::-------------------------------------------------------------------
reserve I for non empty set,
J for ManySortedSet of I,
S for non void non empty ManySortedSign,
i for Element of I,
c for set,
A for MSAlgebra-Family of I,S,
EqR for Equivalence_Relation of I,
U0,U1,U2 for MSAlgebra over S,
s for SortSymbol of S,
o for OperSymbol of S,
f for Function;
registration
let I be set, S;
let AF be MSAlgebra-Family of I,S;
cluster product AF -> non-empty;
coherence by MSUALG_1:def 3;
end;
registration
let X be with_non-empty_elements set;
cluster id X -> non-empty;
coherence;
end;
theorem Th1:
for f,F being Function, A being set st f in product F holds f|A
in product(F|A)
proof
let f,F be Function, A be set;
assume
A1: f in product F;
then dom f = dom F by CARD_3:9;
then
A2: dom (f|A) = dom F /\ A by RELAT_1:61
.= dom (F|A)by RELAT_1:61;
for x be object st x in dom (F|A) holds (f|A).x in (F|A).x
proof
let x be object;
assume
A3: x in dom (F|A);
then x in dom F /\ A by RELAT_1:61;
then
A4: x in dom F by XBOOLE_0:def 4;
(F|A).x = F.x & (f|A).x = f.x by A2,A3,FUNCT_1:47;
hence thesis by A1,A4,CARD_3:9;
end;
hence thesis by A2,CARD_3:9;
end;
theorem Th2:
for A be MSAlgebra-Family of I,S, s be SortSymbol of S, a be non
empty Subset of I, Aa be MSAlgebra-Family of a,S st A|a = Aa holds Carrier(Aa,s
) = (Carrier(A,s))|a
proof
let A be MSAlgebra-Family of I,S, s be SortSymbol of S, a be non empty
Subset of I, Aa be MSAlgebra-Family of a,S such that
A1: A|a = Aa;
dom ((Carrier(A,s))|a) = dom (Carrier(A,s)) /\ a by RELAT_1:61
.= I /\ a by PARTFUN1:def 2
.= a by XBOOLE_1:28;
then reconsider Cas = ((Carrier(A,s))|a) as ManySortedSet of a by
PARTFUN1:def 2;
for i be object st i in a holds (Carrier(Aa,s)).i = Cas.i
proof
let i be object;
assume
A2: i in a;
then reconsider i9 = i as Element of a;
reconsider i99 = i9 as Element of I;
A3: Aa.i9 = A.i9 & ex U1 being MSAlgebra over S st U1 = A.i99 & (Carrier(A
,s) ).i99 = (the Sorts of U1).s by A1,FUNCT_1:49,PRALG_2:def 9;
ex U0 being MSAlgebra over S st U0 = Aa.i & (Carrier(Aa,s) ).i = (the
Sorts of U0).s by A2,PRALG_2:def 9;
hence thesis by A3,FUNCT_1:49;
end;
hence thesis by PBOOLE:3;
end;
theorem Th3:
for i be set, I be non empty set, EqR be Equivalence_Relation of
I, c1,c2 be Element of Class EqR st i in c1 & i in c2 holds c1 = c2
proof
let i be set, I be non empty set, EqR be Equivalence_Relation of I, c1,c2 be
Element of Class EqR such that
A1: i in c1 and
A2: i in c2;
consider x1 be object such that
x1 in I and
A3: c1 = Class(EqR,x1) by EQREL_1:def 3;
A4: [i,x1] in EqR by A1,A3,EQREL_1:19;
consider x2 be object such that
x2 in I and
A5: c2 = Class(EqR,x2) by EQREL_1:def 3;
[i,x2] in EqR by A2,A5,EQREL_1:19;
then Class(EqR,x2) = Class(EqR,i) by A1,EQREL_1:35
.= c1 by A1,A3,A4,EQREL_1:35;
hence thesis by A5;
end;
Lm1: for f be Function, x be set st x in product f holds x is Function;
theorem
for D being non empty set for F being ManySortedFunction of D for C
being with_common_domain functional non empty set st C = rng F for d being
Element of D,e being set st e in DOM C holds F.d.e = (commute F).e.d
proof
let D be non empty set;
let F be ManySortedFunction of D;
set E = union the set of all rng(F.d9) where d9 is Element of D ;
reconsider F9= F as Function;
let C be with_common_domain functional non empty set such that
A1: C = rng F;
A2: rng F9 c= Funcs(DOM C,E)
proof
let x be object;
assume x in rng F9;
then consider d9 be object such that
A3: d9 in dom F and
A4: F.d9 = x by FUNCT_1:def 3;
reconsider d9 as Element of D by A3;
consider Fd be Function such that
A5: Fd = F.d9;
A6: rng Fd c= E
proof
A7: rng Fd in the set of all rng(F.d99) where d99 is Element of D by A5;
let x1 be object;
assume x1 in rng Fd;
hence thesis by A7,TARSKI:def 4;
end;
F.d9 in rng F by A3,FUNCT_1:def 3;
then dom Fd = DOM C by A1,A5,CARD_3:108;
hence thesis by A4,A5,A6,FUNCT_2:def 2;
end;
let d be Element of D,e be set;
assume
A8: e in DOM C;
dom F9 = D by PARTFUN1:def 2;
then F in Funcs(D,Funcs(DOM C,E)) by A2,FUNCT_2:def 2;
hence thesis by A8,FUNCT_6:56;
end;
begin :: Constants of Many Sorted Algebras
definition
let S,U0;
let o be OperSymbol of S;
func const(o,U0) -> set equals
Den(o,U0).{};
correctness;
end;
theorem Th5:
the_arity_of o = {} & Result(o,U0) <> {} implies const(o,U0) in Result(o,U0)
proof
assume that
A1: the_arity_of o = {} and
A2: Result(o,U0) <> {};
dom Den(o,U0) = Args(o,U0) by A2,FUNCT_2:def 1
.= {{}} by A1,PRALG_2:4;
then {} in dom Den(o,U0) by TARSKI:def 1;
then Den(o,U0).{} in rng Den(o,U0) by FUNCT_1:def 3;
hence thesis;
end;
theorem
(the Sorts of U0).s <> {} implies Constants(U0,s) = { const(o,U0)
where o is Element of the carrier' of S : the_result_sort_of o = s &
the_arity_of o = {} }
proof
assume
A1: (the Sorts of U0).s <> {};
thus Constants(U0,s) c= { const(o,U0) where o is Element of the carrier' of
S: the_result_sort_of o = s & the_arity_of o = {} }
proof
let x be object;
assume
A2: x in Constants(U0,s);
ex A being non empty set st A =(the Sorts of U0).s & Constants(U0,s) =
{ a where a is Element of A : ex o be OperSymbol of S st (the Arity of S).o =
{} & (the ResultSort of S).o = s & a in rng Den(o,U0)} by A1,MSUALG_2:def 3;
then consider A being non empty set such that
A =(the Sorts of U0).s and
A3: x in { a where a is Element of A : ex o be OperSymbol of S st (the
Arity of S).o = {} & (the ResultSort of S).o = s & a in rng Den(o,U0)} by A2;
consider a be Element of A such that
A4: a = x and
A5: ex o be OperSymbol of S st (the Arity of S).o = {} & (the
ResultSort of S).o = s & a in rng Den(o,U0) by A3;
consider o1 be OperSymbol of S such that
A6: (the Arity of S).o1 = {} and
A7: (the ResultSort of S).o1 = s and
A8: a in rng Den(o1,U0) by A5;
A9: ex x1 be object st x1 in dom Den(o1,U0) & a = Den(o1,U0).x1 by A8,
FUNCT_1:def 3;
A10: the_result_sort_of o1 = s by A7,MSUALG_1:def 2;
A11: the_arity_of o1 = {} by A6,MSUALG_1:def 1;
then Args(o1,U0) = {{}} by PRALG_2:4;
then x = const(o1,U0) by A4,A9,TARSKI:def 1;
hence thesis by A10,A11;
end;
let x be object;
assume x in { const(o,U0) where o is Element of the carrier' of S :
the_result_sort_of o = s & the_arity_of o = {} };
then consider o being Element of the carrier' of S such that
A12: x = const(o,U0) and
A13: the_result_sort_of o = s and
A14: the_arity_of o = {};
o in the carrier' of S;
then
A15: o in dom (the ResultSort of S) by FUNCT_2:def 1;
A16: Result(o,U0) = ((the Sorts of U0) * the ResultSort of S).o by
MSUALG_1:def 5
.= (the Sorts of U0).((the ResultSort of S).o) by A15,FUNCT_1:13
.= (the Sorts of U0).s by A13,MSUALG_1:def 2;
thus x in Constants(U0,s)
proof
A17: ex o be OperSymbol of S st (the Arity of S).o = {} & (the ResultSort
of S).o = s & x in rng Den(o,U0)
proof
take o;
Args(o,U0) = dom Den(o,U0) & Args(o,U0) = {{}} by A1,A14,A16,
FUNCT_2:def 1,PRALG_2:4;
then {} in dom Den(o,U0) by TARSKI:def 1;
hence thesis by A12,A13,A14,FUNCT_1:def 3,MSUALG_1:def 1,def 2;
end;
consider A being non empty set such that
A18: A =(the Sorts of U0).s and
A19: Constants(U0,s) = { a where a is Element of A : ex o be
OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).o = s & a in
rng Den(o,U0)} by A1,MSUALG_2:def 3;
x is Element of A by A12,A14,A16,A18,Th5;
hence thesis by A19,A17;
end;
end;
theorem Th7:
the_arity_of o = {} implies (commute (OPER A)).o in Funcs(I,Funcs
({{}}, union the set of all Result(o,A.i9) where i9 is Element of I))
proof
set f = (commute (OPER A)).o;
set C = union the set of all Result(o,A.i9) where i9 is Element of I;
commute (OPER A) in Funcs(the carrier' of S, Funcs(I,rng uncurry (OPER A
))) by PRALG_2:6;
then
A1: ex f1 be Function st commute (OPER A) = f1 & dom f1 = the carrier' of S &
rng f1 c= Funcs(I,rng uncurry (OPER A)) by FUNCT_2:def 2;
then f in rng commute (OPER A) by FUNCT_1:def 3;
then
A2: ex fb be Function st fb = f & dom fb = I & rng fb c= rng uncurry (OPER A)
by A1,FUNCT_2:def 2;
assume
A3: the_arity_of o = {};
now
let x be object;
assume x in rng f;
then consider a be object such that
A4: a in dom f and
A5: f.a = x by FUNCT_1:def 3;
f = A?.o;
then reconsider x9 = x as Function by A5;
reconsider a as Element of I by A2,A4;
A6: x9 = (A?.o).a by A5
.= Den(o,A.a) by PRALG_2:7;
then
A7: dom x9 = Args(o,A.a) by FUNCT_2:def 1
.= {{}} by A3,PRALG_2:4;
now
let c be object;
assume c in rng x9;
then consider b be object such that
A8: b in dom x9 and
A9: x9.b = c by FUNCT_1:def 3;
x9.b = const(o,A.a) by A6,A7,A8,TARSKI:def 1;
then
A10: c is Element of Result(o,A.a) by A3,A9,Th5;
Result(o,A.a) in the set of all Result(o,A.i9) where i9 is Element of I;
hence c in C by A10,TARSKI:def 4;
end;
then rng x9 c= C;
hence x in Funcs({{}},C) by A7,FUNCT_2:def 2;
end;
then rng f c= Funcs({{}},C);
hence thesis by A2,FUNCT_2:def 2;
end;
theorem Th8:
the_arity_of o = {} implies const(o,product A) in Funcs(I, union
the set of all Result(o,A.i9) where i9 is Element of I)
proof
set g = (commute (OPER A)).o;
set C = union the set of all Result(o,A.i9) where i9 is Element of I;
assume
A1: the_arity_of o = {};
then
A2: g in Funcs(I,Funcs({{}},C)) by Th7;
reconsider g as Function;
(OPS A).o = (IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)))
by PRALG_2:def 13
.= commute(A?.o) by A1,FUNCOP_1:def 8;
then
A3: const(o,product A) = (commute g).{} by MSUALG_1:def 6;
commute g in Funcs({{}},Funcs(I,C)) by A2,FUNCT_6:55;
then consider g1 be Function such that
A4: g1 = commute g and
A5: dom g1 = {{}} and
A6: rng g1 c= Funcs(I,C) by FUNCT_2:def 2;
{} in {{}} by TARSKI:def 1;
then g1.{} in rng g1 by A5,FUNCT_1:def 3;
hence thesis by A3,A4,A6;
end;
registration
let S,I,o,A;
cluster const (o,product A) -> Relation-like Function-like;
coherence
proof
const(o,product A) is Function
proof
per cases;
suppose
the_arity_of o = {};
then
const(o,product A) in Funcs(I, union the set of all
Result(o,A.i9) where i9 is
Element of I) by Th8;
then ex g be Function st g = const(o,product A) & dom g = I & rng g c=
union the set of all Result(o,A.i9) where i9 is Element of I
by FUNCT_2:def 2;
hence thesis;
end;
suppose
A1: the_arity_of o <> {};
dom ((the Sorts of (product A))*(the_arity_of o)) = dom (
the_arity_of o ) by PRALG_2:3;
then
A2: dom ((the Sorts of (product A))*(the_arity_of o)) <> dom {} by A1;
dom Den(o,product A) = Args(o,product A) by FUNCT_2:def 1
.= product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:3
;
then not {} in dom Den(o,product A) by A2,CARD_3:9;
hence thesis by FUNCT_1:def 2;
end;
end;
hence thesis;
end;
end;
theorem Th9:
for o be OperSymbol of S st the_arity_of o = {} holds (const (o,
product A)).i = const (o,A.i)
proof
let o be OperSymbol of S such that
A1: the_arity_of o = {};
set f = (commute (OPER A)).o, C = union the set of all
Result(o,A.i9) where i9 is Element
of I;
A2: f in Funcs(I,Funcs({{}},C)) by A1,Th7;
(OPS A).o = (IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)))
by PRALG_2:def 13
.= commute(A?.o) by A1,FUNCOP_1:def 8;
then
A3: const(o,product A) = (commute f).{} by MSUALG_1:def 6;
A4: {} in {{}} by TARSKI:def 1;
const (o,A.i) = ((A?.o).i).{} by PRALG_2:7
.= const(o,product A).i by A2,A3,A4,FUNCT_6:56;
hence thesis;
end;
theorem
the_arity_of o = {} & dom f = I & (for i be Element of I holds f.i =
const(o,A.i)) implies f = const(o,product A)
proof
assume that
A1: the_arity_of o = {} and
A2: dom f = I and
A3: for i be Element of I holds f.i = const(o,A.i);
A4: now
let a be object;
assume a in I;
then reconsider a9 = a as Element of I;
thus f.a = const(o,A.a9) by A3
.= (const(o,product A)).a by A1,Th9;
end;
set C = union the set of all Result(o,A.i9) where i9 is Element of I;
const(o,product A) in Funcs(I,C) by A1,Th8;
then ex g2 be Function st g2 = const(o,product A) & dom g2 = I & rng g2 c= C
by FUNCT_2:def 2;
hence thesis by A2,A4;
end;
theorem Th11:
for e be Element of Args(o,U1) st e = {} & the_arity_of o = {} &
Args(o,U1) <> {} & Args(o,U2) <> {} for F be ManySortedFunction of U1,U2 holds
F#e = {}
proof
let e be Element of Args(o,U1) such that
A1: e = {} and
A2: the_arity_of o = {} and
A3: Args(o,U1) <> {} & Args(o,U2) <> {};
reconsider e1 = e as Function by A1;
let F be ManySortedFunction of U1,U2;
A4: dom (F*the_arity_of o) = {} by A2;
then rng (F*the_arity_of o) = {} by RELAT_1:42;
then (F*the_arity_of o) is Function of {},{} by A4,FUNCT_2:1;
then
A5: e1 in product (doms (F*the_arity_of o))
by A1,CARD_3:10,FUNCT_6:23,TARSKI:def 1;
A6: F#e = (Frege(F*the_arity_of o)).e by A3,MSUALG_3:def 5
.= (F*the_arity_of o)..e1 by A5,PRALG_2:def 2;
then reconsider fn = F#e as Function;
dom fn = {} /\ dom e1 by A4,A6,PRALG_1:def 19;
hence thesis;
end;
begin :: Properties of Arguments of operations in Many Sorted Algebras
theorem Th12:
for U1,U2 be non-empty MSAlgebra over S for F be
ManySortedFunction of U1,U2 for x be Element of Args(o,U1) holds x in product
doms (F*the_arity_of o)
proof
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
let x be Element of Args(o,U1);
x in Args(o,U1);
then
A1: x in product ((the Sorts of U1)*(the_arity_of o)) by PRALG_2:3;
A2: dom x = dom the_arity_of o by MSUALG_6:2;
dom F = the carrier of S by PARTFUN1:def 2;
then
A3: rng the_arity_of o c= dom F;
A4: now
let n be object;
assume n in dom doms (F*the_arity_of o);
then n in dom(F*the_arity_of o) by FUNCT_6:def 2;
then n in dom (F*the_arity_of o);
hence n in dom x by A3,A2,RELAT_1:27;
end;
A5: dom x = dom ((the Sorts of U1)*(the_arity_of o)) by A1,CARD_3:9;
A6: now
let n be object;
assume
A7: n in dom (doms (F*the_arity_of o)); then
A8: n in dom the_arity_of o by A2,A4;
then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 3;
then reconsider s1 = (the_arity_of o).n as Element of (the carrier of S);
A9: n in dom (F*the_arity_of o) by A3,A8,RELAT_1:27;
then (F*the_arity_of o).n = F.s1 by FUNCT_1:12;
then
A10: (doms (F*the_arity_of o)).n = dom (F.s1) by A9,FUNCT_6:22
.= (the Sorts of U1).s1 by FUNCT_2:def 1;
n in dom ((the Sorts of U1)*(the_arity_of o)) by A5,A4,A7;
then x.n in ((the Sorts of U1)*(the_arity_of o)).n by A1,CARD_3:9;
hence x.n in (doms (F*the_arity_of o)).n by A5,A4,A7,A10,FUNCT_1:12;
end;
now
let n be object;
assume n in dom x; then
A11: n in dom (F*the_arity_of o) by A3,A2,RELAT_1:27;
n in dom(F*the_arity_of o) by A11;
hence n in dom doms (F*the_arity_of o) by FUNCT_6:def 2;
end;
then
A12: dom x c= dom doms (F*the_arity_of o);
dom doms (F*the_arity_of o) c= dom x by A4;
then dom x = dom (doms (F*the_arity_of o)) by A12;
hence thesis by A6,CARD_3:9;
end;
theorem Th13:
for U1,U2 be non-empty MSAlgebra over S
for F be ManySortedFunction of U1,U2
for x be Element of Args(o,U1) for n be set st
n in dom the_arity_of o holds (F#x).n = F.((the_arity_of o)/.n).(x.n)
proof
let U1,U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
let x be Element of Args(o,U1);
let n be set such that
A1: n in dom the_arity_of o;
dom F = the carrier of S by PARTFUN1:def 2; then
a1: rng the_arity_of o c= dom F; then
A2: n in dom (F*the_arity_of o) by A1,RELAT_1:27;
B2: dom x = dom the_arity_of o by MSUALG_6:2;
dom (F*the_arity_of o) = dom the_arity_of o by a1,RELAT_1:27; then
dom ((F*the_arity_of o)..x) = (dom the_arity_of o) /\ dom x
by PRALG_1:def 19
.= dom the_arity_of o by B2; then
a2: n in dom ((F*the_arity_of o)..x) by A1;
A3: x in product doms (F*the_arity_of o) by Th12;
thus (F#x).n = ((Frege(F*the_arity_of o)).x).n by MSUALG_3:def 5
.= ((F*the_arity_of o)..x).n by A3,PRALG_2:def 2
.= ((F*the_arity_of o).n).(x.n) by a2,PRALG_1:def 19
.= (F.((the_arity_of o).n)).(x.n) by A2,FUNCT_1:12
.= F.((the_arity_of o)/.n).(x.n) by A1,PARTFUN1:def 6;
end;
theorem Th14:
for x be Element of Args(o,product A) holds x in Funcs (dom (
the_arity_of o),Funcs (I,union the set of all
(the Sorts of A.i9).s9 where i9 is Element of
I,s9 is Element of (the carrier of S) ))
proof
let x be Element of Args(o,product A);
set C = union the set of all
(the Sorts of A.i9).s9 where i9 is Element of I, s9 is
Element of (the carrier of S) ;
consider x1 be Function such that
A1: x1 = x;
x in Args(o,product A);
then
A2: x in product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:3;
dom (SORTS A) = the carrier of S by PARTFUN1:def 2;
then
A3: rng (the_arity_of o) c= dom (SORTS A);
now
let c be object;
assume c in rng x1;
then consider n be object such that
A4: n in dom x1 and
A5: x1.n = c by FUNCT_1:def 3;
A6: n in dom ((SORTS A)*(the_arity_of o)) by A2,A1,A4,CARD_3:9;
then n in dom (the_arity_of o) by A3,RELAT_1:27;
then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 3;
then reconsider s1 = (the_arity_of o).n as Element of (the carrier of S);
x1.n in ((SORTS A)*(the_arity_of o)).n by A2,A1,A6,CARD_3:9;
then x1.n in (SORTS A).s1 by A6,FUNCT_1:12;
then x1.n in product Carrier(A,s1) by PRALG_2:def 10;
then consider g be Function such that
A7: g = x1.n and
A8: dom g = dom Carrier(A,s1) and
A9: for i9 be object st i9 in dom (Carrier(A,s1)) holds g.i9 in (Carrier
(A,s1)).i9 by CARD_3:def 5;
now
let c1 be object;
assume c1 in rng g;
then consider i1 be object such that
A10: i1 in dom g and
A11: g.i1 = c1 by FUNCT_1:def 3;
reconsider i1 as Element of I by A8,A10;
ex U0 being MSAlgebra over S st U0 = A.i1 & (Carrier(A,s1 )).i1 = (
the Sorts of U0).s1 by PRALG_2:def 9;
then
A12: g.i1 in (the Sorts of A.i1).s1 by A8,A9,A10;
(the Sorts of A.i1).s1 in the set of all
(the Sorts of A.i9).s9 where i9 is
Element of I, s9 is Element of (the carrier of S) ;
hence c1 in C by A11,A12,TARSKI:def 4;
end;
then
A13: rng g c= C;
dom g = I by A8,PARTFUN1:def 2;
hence c in Funcs(I,C) by A5,A7,A13,FUNCT_2:def 2;
end;
then
A14: rng x1 c= Funcs(I,C);
dom x = dom ((SORTS A)*(the_arity_of o)) by A2,CARD_3:9
.= dom (the_arity_of o) by A3,RELAT_1:27;
hence thesis by A1,A14,FUNCT_2:def 2;
end;
theorem Th15:
for x be Element of Args(o,product A) for n be set st n in dom (
the_arity_of o) holds x.n in product Carrier(A,(the_arity_of o)/.n)
proof
let x be Element of Args(o,product A);
let n be set such that
A1: n in dom (the_arity_of o);
dom (SORTS A) = the carrier of S by PARTFUN1:def 2;
then rng (the_arity_of o) c= dom (SORTS A);
then
A2: n in dom ((SORTS A)*(the_arity_of o)) by A1,RELAT_1:27;
x in Args(o,product A);
then x in product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:3;
then x.n in ((SORTS A)*(the_arity_of o)).n by A2,CARD_3:9;
then x.n in (SORTS A).((the_arity_of o).n) by A2,FUNCT_1:12;
then x.n in (SORTS A).((the_arity_of o)/.n) by A1,PARTFUN1:def 6;
hence thesis by PRALG_2:def 10;
end;
theorem Th16:
for i be Element of I for n be set st n in dom(the_arity_of o)
for s be SortSymbol of S st s = (the_arity_of o).n for y be Element of Args(o,
product A) for g be Function st g = y.n holds g.i in (the Sorts of A.i).s
proof
let i be Element of I;
let n be set;
assume n in dom(the_arity_of o);
then
A1: n in dom ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:3;
let s be SortSymbol of S such that
A2: s = (the_arity_of o).n;
let y be Element of Args(o,product A);
y in Args(o,product A);
then
A3: y in product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:3;
let g be Function;
assume g = y.n;
then g in ((the Sorts of (product A))*(the_arity_of o)).n by A1,A3,CARD_3:9;
then g in (the Sorts of (product A)).s by A2,A1,FUNCT_1:12;
then
A4: g in product Carrier(A,s) by PRALG_2:def 10;
i in I;
then
A5: i in dom (Carrier(A,s)) by PARTFUN1:def 2;
ex U0 being MSAlgebra over S st U0 = A.i & (Carrier(A,s)) .i = (the
Sorts of U0).s by PRALG_2:def 9;
hence thesis by A5,A4,CARD_3:9;
end;
theorem Th17:
for y be Element of Args(o,product A) st (the_arity_of o) <> {}
holds (commute y) in product doms (A?.o)
proof
let y be Element of Args(o,product A);
set D = union the set of all
(the Sorts of A.i9).s9 where i9 is Element of I,s9 is
Element of (the carrier of S) ;
A1: y in Funcs (dom (the_arity_of o),Funcs (I,D)) by Th14;
assume (the_arity_of o) <> {};
then commute y in Funcs (I,Funcs (dom (the_arity_of o),D)) by A1,FUNCT_6:55;
then
A2: ex f be Function st f = commute y & dom f = I & rng f c= Funcs (dom (
the_arity_of o),D) by FUNCT_2:def 2;
A3: now
let i1 be object;
assume i1 in dom (doms (A?.o));
then reconsider ii =i1 as Element of I by PRALG_2:11;
A4: now
let n be object;
assume
A5: n in dom ((the Sorts of A.ii)*(the_arity_of o));
then
A6: n in dom (the_arity_of o) by PRALG_2:3;
then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 3;
then reconsider s1 = (the_arity_of o).n as SortSymbol of S;
A7: ex ff be Function st ff = y & dom ff = dom (the_arity_of o) & rng ff
c= Funcs(I,D) by A1,FUNCT_2:def 2;
then n in dom y by A5,PRALG_2:3;
then y.n in rng y by FUNCT_1:def 3;
then consider g be Function such that
A8: g = y.n and
dom g = I and
rng g c= D by A7,FUNCT_2:def 2;
((commute y).ii).n = g.ii & g.ii in (the Sorts of A.ii).s1 by A1,A6,A8
,Th16,FUNCT_6:56;
hence ((commute y).ii).n in ((the Sorts of A.ii)*(the_arity_of o)).n by
A5,FUNCT_1:12;
end;
(commute y).ii in rng (commute y) by A2,FUNCT_1:def 3;
then
ex h be Function st h = (commute y).ii & dom h = dom ( the_arity_of o)
& rng h c= D by A2,FUNCT_2:def 2;
then dom((commute y).ii) = dom ((the Sorts of A.ii)*(the_arity_of o)) by
PRALG_2:3;
then (commute y).ii in product ((the Sorts of A.ii)*(the_arity_of o)) by A4
,CARD_3:9;
then (commute y).ii in Args(o,A.ii) by PRALG_2:3;
hence (commute y).i1 in (doms (A?.o)).i1 by PRALG_2:11;
end;
dom (commute y) = dom (doms (A?.o)) by A2,PRALG_2:11;
hence thesis by A3,CARD_3:9;
end;
theorem Th18:
for y be Element of Args(o,product A) st the_arity_of o <> {}
holds y in dom (Commute Frege(A?.o))
proof
let y be Element of Args(o,product A);
set D = union the set of all
(the Sorts of A.ii).ss where ii is Element of I,ss is
Element of (the carrier of S) ;
assume
A1: the_arity_of o <> {};
then (commute y) in product doms (A?.o) by Th17;
then
A2: (commute y) in dom (Frege(A?.o)) by PARTFUN1:def 2;
y in Funcs (dom (the_arity_of o),Funcs (I,D)) by Th14;
then y = commute commute y by A1,FUNCT_6:57;
hence thesis by A2,PRALG_2:def 1;
end;
theorem Th19:
for I be set, S be non void non empty ManySortedSign, A be
MSAlgebra-Family of I,S, o be OperSymbol of S for x be Element of Args(o,
product A) holds Den(o,product A).x in product Carrier(A,the_result_sort_of o)
proof
let I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family
of I,S, o be OperSymbol of S;
let x be Element of Args(o,product A);
Result(o,product A) = (SORTS A).(the_result_sort_of o) by PRALG_2:3
.= product Carrier(A,the_result_sort_of o) by PRALG_2:def 10;
hence thesis;
end;
theorem Th20:
for I,S,A,i for o be OperSymbol of S st (the_arity_of o) <> {}
for U1 be non-empty MSAlgebra over S for x be Element of Args(o,product A)
holds (commute x).i is Element of Args(o,A.i)
proof
let I,S,A,i;
let o be OperSymbol of S such that
A1: (the_arity_of o) <> {};
let U1 be non-empty MSAlgebra over S;
let x be Element of Args(o,product A);
i in I;
then
A2: i in dom (doms(A?.o)) by PRALG_2:11;
(commute x) in product doms(A?.o) by A1,Th17;
then (commute x).i in doms(A?.o).i by A2,CARD_3:9;
hence thesis by PRALG_2:11;
end;
theorem Th21:
for I,S,A,i,o for x be Element of Args(o,product A) for n be set
st n in dom(the_arity_of o) for f be Function st f = x.n holds ((commute x).i).
n = f.i
proof
let I,S,A,i,o;
let x be Element of Args(o,product A);
let n be set such that
A1: n in dom the_arity_of o;
set C = union the set of all (the Sorts of A.i9).s9 where
i9 is Element of I,s9 is Element of (the carrier of S);
A2: x in Funcs (dom (the_arity_of o),Funcs (I,C)) by Th14;
let g be Function;
assume g = x.n;
hence thesis by A1,A2,FUNCT_6:56;
end;
theorem Th22:
for o be OperSymbol of S st (the_arity_of o) <> {}
for y be Element of Args(o,product A), i9 be Element of I
for g be Function st g = Den(o,product A).y holds
g.i9 = Den(o,A.i9).((commute y).i9)
proof
let o be OperSymbol of S such that
A1: the_arity_of o <> {};
let y be Element of Args(o,product A), i9 be Element of I;
A2: y in dom (Commute Frege(A?.o)) by A1,Th18;
A3: commute y in product doms (A?.o) by A1,Th17;
A4: Den(o,product A) = (OPS A).o by MSUALG_1:def 6
.= IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o))
by PRALG_2:def 13
.= (Commute Frege(A?.o)) by A1,FUNCOP_1:def 8;
set C = union the set of all (the Sorts of A.i9).s9 where
i9 is Element of I, s9 is Element of the carrier of S;
y in Funcs (dom the_arity_of o,Funcs(I,C)) by Th14; then
commute y in Funcs(I,Funcs(dom (the_arity_of o),C)) by A1,FUNCT_6:55; then
WW: dom commute y = I by FUNCT_2:92;
dom (A?.o) = I by PARTFUN1:def 2; then
a5: dom ((A?.o)..commute y) = I /\ dom commute y by PRALG_1:def 19
.= I by WW;
let g be Function;
assume g = Den(o,product A).y;
then g = (Frege(A?.o)).(commute y) by A4,A2,PRALG_2:def 1
.= (A?.o)..(commute y) by A3,PRALG_2:def 2;
then g.i9 = ((A?.o).i9).((commute y).i9) by a5,PRALG_1:def 19
.= Den(o,A.i9).((commute y).i9) by PRALG_2:7;
hence thesis;
end;
begin :: The Projection of Family of Many Sorted Algebras
definition
let I,S;
let A be MSAlgebra-Family of I,S, i be Element of I;
func proj(A,i) -> ManySortedFunction of product A,A.i means
:Def2:
for s be Element of S holds it.s = proj (Carrier(A,s), i);
existence
proof
deffunc G(Element of S) = proj (Carrier(A,$1), i);
consider F be ManySortedSet of the carrier of S such that
A1: for s be Element of S holds F.s = G(s) from PBOOLE:sch 5;
F is ManySortedFunction of product A,A.i
proof
let s be object such that
A2: s in the carrier of S;
F.s is Function of (the Sorts of product A).s, (the Sorts of A.i).s
proof
reconsider s9 = s as Element of S by A2;
F.s = proj (Carrier(A,s9),i) by A1;
then reconsider F9 = F.s as Function;
A3: rng F9 c= (the Sorts of A.i).s
proof
let y be object;
A4: dom (Carrier(A,s9)) = I & ex U0 being MSAlgebra over S st U0 =
A.i & ( Carrier(A,s9) ).i = (the Sorts of U0).s9 by PARTFUN1:def 2
,PRALG_2:def 9;
assume y in rng F9;
then y in rng (proj (Carrier(A,s9),i)) by A1;
then consider x1 be object such that
A5: x1 in dom (proj (Carrier(A,s9),i)) and
A6: y = (proj (Carrier(A,s9),i)).x1 by FUNCT_1:def 3;
A7: x1 in product (Carrier(A,s9)) by A5;
then reconsider x1 as Function;
y = x1.i by A5,A6,CARD_3:def 16;
hence thesis by A7,A4,CARD_3:9;
end;
dom F9 = dom (proj (Carrier(A,s9),i)) by A1
.= product (Carrier(A,s9)) by CARD_3:def 16
.= (the Sorts of product A).s by PRALG_2:def 10;
hence thesis by A2,A3,FUNCT_2:def 1,RELSET_1:4;
end;
hence thesis;
end;
then reconsider F9 = F as ManySortedFunction of product A,A.i;
take F9;
thus thesis by A1;
end;
uniqueness
proof
let F,G be ManySortedFunction of product A,A.i such that
A8: for s be Element of S holds F.s = proj (Carrier(A,s), i) and
A9: for s be Element of S holds G.s = proj (Carrier(A,s), i);
now
let s9 be object;
assume s9 in (the carrier of S);
then reconsider s99 = s9 as Element of S;
thus F.s9 = proj (Carrier(A,s99), i) by A8
.= G.s9 by A9;
end;
hence F = G;
end;
end;
theorem Th23:
for x be Element of Args(o,product A) st the_arity_of o <> {}
for i be Element of I holds proj(A,i)#x = (commute x).i
proof
let x be Element of Args(o,product A) such that
A1: the_arity_of o <> {};
set C = union the set of all
(the Sorts of A.i9).s9 where i9 is Element of I,
s9 is Element of the carrier of S;
let i be Element of I;
A2: x in Funcs (dom the_arity_of o,Funcs(I,C)) by Th14; then
A3: commute x in Funcs(I,Funcs(dom (the_arity_of o),C)) by A1,FUNCT_6:55;
then dom commute x = I by FUNCT_2:92;
then
A4: (commute x).i in rng commute x by FUNCT_1:def 3;
SS: dom x = dom the_arity_of o by MSUALG_6:2;
A5: now
A6: rng x c= Funcs(I,C) by A2,FUNCT_2:92;
let n be object such that
A7: n in dom the_arity_of o;
x.n in product Carrier(A,(the_arity_of o)/.n) by A7,Th15;
then
A8: x.n in dom (proj (Carrier(A,(the_arity_of o)/.n),i)) by CARD_3:def 16;
n in dom x by A2,A7,FUNCT_2:92;
then x.n in rng x by FUNCT_1:def 3;
then consider g be Function such that
A9: g = x.n and
dom g = I and
rng g c= C by A6,FUNCT_2:def 2;
thus ((proj(A,i))#x).n = ((proj(A,i)).((the_arity_of o)/.n)).(x.n) by A7
,Th13
.= (proj (Carrier(A,(the_arity_of o)/.n),i)).(x.n) by Def2
.= g.i by A9,A8,CARD_3:def 16
.= ((commute x).i).n by A2,A7,A9,FUNCT_6:56;
end;
A10: x in product doms ((proj(A,i))*the_arity_of o) by Th12;
rng commute x c= Funcs(dom (the_arity_of o), C) by A3,FUNCT_2:92;
then
A11: dom ((commute x).i) = dom the_arity_of o by A4,FUNCT_2:92;
dom (proj(A,i)) = the carrier of S by PARTFUN1:def 2; then
A12: rng the_arity_of o c= dom (proj(A,i));
dom ((proj(A,i))#x) = dom ((Frege((proj(A,i))*the_arity_of o)).x) by
MSUALG_3:def 5
.= dom (((proj(A,i))*the_arity_of o)..x) by A10,PRALG_2:def 2
.= dom ((proj(A,i))*the_arity_of o) /\ dom x by PRALG_1:def 19
.= dom (the_arity_of o) /\ dom x by A12,RELAT_1:27;
hence thesis by A11,A5,SS;
end;
theorem
for i be Element of I for A be MSAlgebra-Family of I,S holds proj(A,i)
is_homomorphism product A,A.i
proof
let i be Element of I;
let A be MSAlgebra-Family of I,S;
thus proj(A,i) is_homomorphism product A,A.i
proof
let o be OperSymbol of S such that
Args(o,product A) <> {};
let x be Element of Args(o,product A);
set F = proj(A,i), s = the_result_sort_of o;
o in the carrier' of S;
then
A1: o in dom (the ResultSort of S) by FUNCT_2:def 1;
A2: Result(o,product A) = ((the Sorts of product A) * the ResultSort of S)
.o by MSUALG_1:def 5
.= (the Sorts of product A).((the ResultSort of S).o) by A1,FUNCT_1:13
.= (SORTS A).s by MSUALG_1:def 2
.= product Carrier(A,s) by PRALG_2:def 10;
thus (F.s).(Den(o,product A).x) = Den(o,A.i).(F#x)
proof
per cases;
suppose
A3: the_arity_of o = {};
then const(o,product A) in product(Carrier(A,s)) by A2,Th5;
then
A4: const(o,product A) in dom (proj (Carrier(A,s),i)) by CARD_3:def 16;
A5: Args(o,product A) = {{}} by A3,PRALG_2:4;
then
A6: x = {} by TARSKI:def 1;
(F.s).(Den(o,product A).x) = (F.s).(const(o,product A)) by A5,
TARSKI:def 1
.= (proj (Carrier(A,s),i)).(const(o,product A)) by Def2
.= (const(o,product A)).i by A4,CARD_3:def 16
.= const(o,A.i) by A3,Th9
.= Den(o,A.i).(F#x) by A3,A6,Th11;
hence thesis;
end;
suppose
A7: the_arity_of o <> {};
reconsider D = (Den(o,product A).x) as Function by A2;
(Den(o,product A).x) in product Carrier(A,s) by A2;
then
A8: (Den(o,product A).x) in dom (proj (Carrier(A,s),i)) by CARD_3:def 16;
(F.s).(Den(o,product A).x) = (proj (Carrier(A,s),i)).(Den(o,
product A).x) by Def2
.= D.i by A8,CARD_3:def 16
.= (Den(o,A.i)).((commute x).i) by A7,Th22
.= (Den(o,A.i)).(proj(A,i)#x) by A7,Th23;
hence thesis;
end;
end;
end;
end;
theorem Th25:
for U1 be non-empty MSAlgebra over S for F being
ManySortedFunction of I st (for i be Element of I holds ex F1 being
ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds F
in Funcs(I,Funcs(the carrier of S, the set of all
F.i9.s1 where s1 is SortSymbol of S,i9 is
Element of I )) & (commute F).s.i = F.i.s
proof
let U1 be non-empty MSAlgebra over S;
let F be ManySortedFunction of I such that
A1: for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i
st F1 = F.i & F1 is_homomorphism U1,A.i;
set FS = the set of all F.i9.s1 where
s1 is SortSymbol of S,i9 is Element of I;
set CA = the carrier of S;
A2: rng F c= Funcs(CA,FS)
proof
let x be object;
assume x in rng F;
then consider i9 be object such that
A3: i9 in dom F and
A4: F.i9 = x by FUNCT_1:def 3;
reconsider i1 = i9 as Element of I by A3;
consider F9 being ManySortedFunction of U1,A.i1 such that
A5: F9 = F.i1 and
F9 is_homomorphism U1,A.i1 by A1;
A6: rng F9 c= FS
proof
let x9 be object;
assume x9 in rng F9;
then consider s9 be object such that
A7: s9 in dom F9 and
A8: F9.s9 = x9 by FUNCT_1:def 3;
s9 is SortSymbol of S by A7;
hence thesis by A5,A8;
end;
dom F9 = CA by PARTFUN1:def 2;
hence thesis by A4,A5,A6,FUNCT_2:def 2;
end;
A9: dom F = I by PARTFUN1:def 2;
hence F in Funcs(I,Funcs(CA,FS)) by A2,FUNCT_2:def 2;
F in Funcs(I,Funcs(CA,FS)) by A9,A2,FUNCT_2:def 2;
hence thesis by FUNCT_6:56;
end;
theorem Th26:
for U1 be non-empty MSAlgebra over S for F being
ManySortedFunction of I st (for i be Element of I holds ex F1 being
ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds
(commute F).s in Funcs(I,Funcs((the Sorts of U1).s, union the set of all
(the Sorts of A.i9).s1 where i9 is Element of I,s1 is SortSymbol of S ))
proof
let U1 be non-empty MSAlgebra over S;
let F be ManySortedFunction of I such that
A1: for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i
st F1 = F.i & F1 is_homomorphism U1,A.i;
set SU = the Sorts of U1, CA = the carrier of S, SA = union the set of all
(the Sorts of A
.i9).s1 where i9 is Element of I,s1 is SortSymbol of S;
set SA9 = the set of all
(the Sorts of A.i9).s1 where i9 is Element of I,s1 is SortSymbol of S;
set FS =
the set of all F.i9.s1 where s1 is SortSymbol of S,i9 is Element of
I;
F in Funcs(I,Funcs(CA,FS)) by A1,Th25;
then commute F in Funcs(CA,Funcs(I,FS)) by FUNCT_6:55;
then consider F9 be Function such that
A2: F9 = commute F & dom F9 = CA and
A3: rng F9 c= Funcs(I,FS) by FUNCT_2:def 2;
(commute F).s in rng F9 by A2,FUNCT_1:def 3;
then
A4: ex F2 be Function st F2 = (commute F).s & dom F2 = I & rng F2 c= FS by A3,
FUNCT_2:def 2;
rng ((commute F).s) c= Funcs(SU.s,SA)
proof
let x9 be object;
assume x9 in rng ((commute F).s);
then consider i9 be object such that
A5: i9 in dom ((commute F).s) and
A6: x9 = ((commute F).s).i9 by FUNCT_1:def 3;
reconsider i1 = i9 as Element of I by A4,A5;
consider F9 be ManySortedFunction of U1,A.i1 such that
A7: F9 = F.i1 and
F9 is_homomorphism U1,A.i1 by A1;
(the Sorts of A.i1).s c= SA
proof
A8: (the Sorts of A.i1).s in SA9;
let y be object;
assume y in (the Sorts of A.i1).s;
hence thesis by A8,TARSKI:def 4;
end;
then
A9: dom (F9.s) = SU.s & rng (F9.s) c= SA by FUNCT_2:def 1;
x9 = F9.s by A1,A6,A7,Th25;
hence thesis by A9,FUNCT_2:def 2;
end;
hence thesis by A4,FUNCT_2:def 2;
end;
theorem Th27:
for U1 be non-empty MSAlgebra over S
for F being ManySortedFunction of I st
(for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st
F1 = F.i & F1 is_homomorphism U1,A.i)
for F9 be ManySortedFunction of U1,A.i st F9 = F.i
for x be set st x in (the Sorts of U1).s
for f be Function st f = (commute((commute F).s)).x holds f.i = F9.s.x
proof
let U1 be non-empty MSAlgebra over S;
set SU = the Sorts of U1, SA = union the set of all
(the Sorts of A.i9).s1 where i9 is
Element of I,s1 is SortSymbol of S ;
let F be ManySortedFunction of I such that
A1: for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i
st F1 = F.i & F1 is_homomorphism U1,A.i;
A2: (commute F).s in Funcs (I,Funcs(SU.s,SA)) by A1,Th26;
then dom ((commute F).s) = I by FUNCT_2:92;
then
A3: ((commute F).s).i in rng ((commute F).s) by FUNCT_1:def 3;
reconsider f9 = (commute F).s as Function;
rng ((commute F).s) c= Funcs(SU.s,SA) by A2,FUNCT_2:92;
then consider g be Function such that
A4: g = f9.i and
dom g = SU.s and
rng g c= SA by A3,FUNCT_2:def 2;
let F9 be ManySortedFunction of U1,A.i such that
A5: F9 = F.i;
let x1 be set such that
A6: x1 in (the Sorts of U1).s;
let f be Function such that
A7: f = (commute((commute F).s)).x1;
g = F9.s by A1,A5,A4,Th25;
hence thesis by A6,A7,A2,A4,FUNCT_6:56;
end;
theorem Th28:
for U1 be non-empty MSAlgebra over S
for F being ManySortedFunction of I st
(for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st
F1 = F.i & F1 is_homomorphism U1,A.i)
for x be set st x in (the Sorts of U1).s holds
(commute ((commute F).s)).x in product (Carrier(A,s))
proof
let U1 be non-empty MSAlgebra over S;
set SU = the Sorts of U1, SA = union the set of all
(the Sorts of A.i9).s1 where i9 is
Element of I,s1 is SortSymbol of S ;
let F be ManySortedFunction of I such that
A1: for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i
st F1 = F.i & F1 is_homomorphism U1,A.i;
(commute F).s in Funcs (I,Funcs(SU.s,SA)) by A1,Th26;
then commute ((commute F).s) in Funcs (SU.s,Funcs(I,SA)) by FUNCT_6:55;
then consider f9 be Function such that
A2: f9 = (commute (commute F).s) and
A3: dom f9 = SU.s and
A4: rng f9 c= Funcs(I,SA) by FUNCT_2:def 2;
let x be set such that
A5: x in (the Sorts of U1).s;
f9.x in rng f9 by A5,A3,FUNCT_1:def 3;
then consider f be Function such that
A6: f = (commute (commute F).s).x and
A7: dom f = I and
rng f c= SA by A2,A4,FUNCT_2:def 2;
A8: now
let i1 be object;
assume i1 in dom ((Carrier(A,s)));
then reconsider i9 = i1 as Element of I;
consider F1 be ManySortedFunction of U1,A.i9 such that
A9: F1 = F.i9 and
F1 is_homomorphism U1,A.i9 by A1;
x in dom (F1.s) by A5,FUNCT_2:def 1;
then
A10: (ex U0 being MSAlgebra over S st U0 = A.i9 & (Carrier(A,s )).i9 = (
the Sorts of U0).s )& F1.s.x in rng (F1.s) by FUNCT_1:def 3,PRALG_2:def 9;
f.i9 = F1.s.x by A1,A5,A6,A9,Th27;
hence ((commute ((commute F).s)).x).i1 in ((Carrier(A,s))).i1 by A6,A10;
end;
dom ((commute (commute F).s).x) = dom (Carrier(A,s)) by A6,A7,PARTFUN1:def 2;
hence thesis by A8,CARD_3:9;
end;
theorem
for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of
I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st
F1 = F.i & F1 is_homomorphism U1,A.i) holds ex H being ManySortedFunction of U1
,(product A) st H is_homomorphism U1,(product A) & for i be Element of I holds
proj(A,i) ** H = F.i
proof
let U1 be non-empty MSAlgebra over S;
let F be ManySortedFunction of I such that
A1: for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i
st F1 = F.i & F1 is_homomorphism U1,A.i;
set SU = the Sorts of U1, CA = the carrier of S, SA = union the set of all
(the Sorts of A
.i9).s1 where i9 is Element of I,s1 is SortSymbol of S ;
deffunc G(Element of S) = commute((commute F).$1);
consider H being ManySortedSet of (the carrier of S) such that
A2: for s9 be Element of (the carrier of S) holds H.s9 = G(s9) from
PBOOLE:sch 5;
now
let s9 be object;
assume
A3: s9 in the carrier of S;
then reconsider s99 = s9 as SortSymbol of S;
(commute F).s9 in Funcs (I,Funcs(SU.s9,SA)) by A1,A3,Th26;
then commute ((commute F).s9) in Funcs (SU.s9,Funcs(I,SA)) by A3,FUNCT_6:55
;
then H.s9 in Funcs(SU.s9,Funcs(I,SA)) by A2,A3;
then consider Hs be Function such that
A4: Hs = H.s9 and
A5: dom Hs = SU.s9 and
A6: rng Hs c= Funcs(I,SA) by FUNCT_2:def 2;
rng Hs c= (the Sorts of (product A)).s9
proof
let x be object;
assume
A7: x in rng Hs;
then consider f be Function such that
A8: f = x and
A9: dom f = I and
rng f c= SA by A6,FUNCT_2:def 2;
consider x1 be object such that
A10: x1 in dom Hs and
A11: Hs.x1 = f by A7,A8,FUNCT_1:def 3;
A12: now
let i9 be object;
assume i9 in dom Carrier(A,s99);
then reconsider i99 = i9 as Element of I;
consider F9 be ManySortedFunction of U1,A.i99 such that
A13: F9 = F.i99 and
F9 is_homomorphism U1,A.i99 by A1;
H.s99 = commute ((commute F).s99) by A2;
then
A14: f.i99 = F9.s99.x1 by A1,A4,A5,A10,A11,A13,Th27;
dom (F9.s99) = dom Hs by A5,FUNCT_2:def 1;
then
A15: F9.s9.x1 in rng (F9.s9) by A10,FUNCT_1:def 3;
(ex U0 being MSAlgebra over S st U0 = A.i99 & (Carrier(A, s99)).
i99 =(the Sorts of U0).s99 )& rng (F9.s99) c= (the Sorts of A.i99).s99 by
PRALG_2:def 9;
hence f.i9 in Carrier(A,s99).i9 by A14,A15;
end;
dom Carrier(A,s99) = dom f by A9,PARTFUN1:def 2;
then f in product Carrier(A,s99) by A12,CARD_3:9;
hence thesis by A8,PRALG_2:def 10;
end;
hence
H.s9 is Function of (the Sorts of U1).s9, (the Sorts of (product A)).
s9 by A3,A4,A5,FUNCT_2:def 1,RELSET_1:4;
end;
then reconsider H as ManySortedFunction of U1,(product A) by PBOOLE:def 15;
A16: H is_homomorphism U1,(product A)
proof
let o be OperSymbol of S such that
Args(o,U1) <> {};
let x be Element of Args(o,U1);
set s9 = the_result_sort_of o;
A17: Result(o,U1) = (the Sorts of U1).(the_result_sort_of o) by PRALG_2:3;
then
A18: (Den(o,U1).x) in SU.s9;
thus (H.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,(product A)).(H#x)
proof
per cases;
suppose
A19: the_arity_of o = {};
set f = (commute ((commute F).s9)).const(o,U1);
Args(o,U1) = {{}} by A19,PRALG_2:4;
then
A20: x = {} by TARSKI:def 1;
A21: now
let i9 be object;
assume i9 in I;
then reconsider ii = i9 as Element of I;
consider F1 be ManySortedFunction of U1,A.ii such that
A22: F1 = F.ii and
A23: F1 is_homomorphism U1,A.ii by A1;
A24: F1#x = {} by A19,A20,Th11;
thus f.i9 = (F1.(the_result_sort_of o)).(Den(o,U1).x) by A1,A17,A20
,A22,Th27
.= const(o,A.ii) by A23,A24
.= (const(o,product A)).i9 by A19,Th9;
end;
const(o,product A) in Funcs(I,union the set of all
Result(o,A.i1) where i1 is
Element of I) by A19,Th8;
then
A25: ex Co be Function st Co = const(o,product A) & dom Co = I & rng Co
c= union the set of all Result(o,A.i1) where i1 is Element of I by
FUNCT_2:def 2;
f in product Carrier(A,s9) by A1,A18,A20,Th28;
then dom f = I by PARTFUN1:def 2; then
A26: f = const(o,product A) by A25,A21;
H#x = {} by A19,A20,Th11;
hence thesis by A2,A20,A26;
end;
suppose
A27: the_arity_of o <> {};
A28: Den(o,product A) = (OPS A).o by MSUALG_1:def 6
.= IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)) by
PRALG_2:def 13
.= Commute Frege(A?.o) by A27,FUNCOP_1:def 8;
A29: now
let y be Element of Args(o,product A);
(commute y) in product doms (A?.o) by A27,Th17;
then
A30: (commute y) in dom (Frege(A?.o)) by PARTFUN1:def 2;
y in dom (Commute Frege(A?.o)) by A27,Th18;
then Den(o,product A).y = (Frege(A?.o)).(commute y) by A28,
PRALG_2:def 1;
hence Den(o,product A).y in rng (Frege(A?.o)) by A30,FUNCT_1:def 3;
end;
then reconsider f1 = Den(o,(product A)).(H#x) as Function by PRALG_2:8;
f1 in rng (Frege(A?.o)) by A29;
then
A31: dom f1 = I by PRALG_2:9;
set D = union the set of all (the Sorts of A.i9).ss where
i9 is Element of I,ss is Element of (the carrier of S);
set f = (commute ((commute F).s9)).(Den(o,U1).x);
A32: (H#x) in Funcs (dom (the_arity_of o),Funcs (I,D)) by Th14;
A33: now
let i9 be object;
assume i9 in I;
then reconsider ii = i9 as Element of I;
consider F1 be ManySortedFunction of U1,A.ii such that
A34: F1 = F.ii and
A35: F1 is_homomorphism U1,A.ii by A1;
A36: (F1.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,A.ii).(F1#x)
by A35;
x in Args(o,U1);
then
A40: x in product ((the Sorts of U1)*(the_arity_of o)) by PRALG_2:3;
then
A41: dom x = dom ((the Sorts of U1)*(the_arity_of o)) by CARD_3:9;
A42: dom x = dom the_arity_of o by MSUALG_6:2;
A37: now
let n be object;
assume
A38: n in dom (the_arity_of o);
then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 3;
then reconsider
s1 = (the_arity_of o).n as Element of (the carrier of S
);
A39: (F1#x).n = F1.((the_arity_of o)/.n).(x.n) by A38,Th13
.= F1.s1.(x.n) by A38,PARTFUN1:def 6;
x.n in ((the Sorts of U1)*(the_arity_of o)).n by A38,A40,A41,A42,
CARD_3:9;
then
A43: (x.n) in SU.s1 by A38,A42,A41,FUNCT_1:12;
A44: (H#x).n = H.((the_arity_of o)/.n).(x.n) by A38,Th13
.= H.s1.(x.n) by A38,PARTFUN1:def 6
.= (commute ((commute F).s1)).(x.n) by A2;
then reconsider g = (H#x).n as Function;
thus ((commute (H#x)).ii).n = g.ii by A32,A38,FUNCT_6:56
.= (F1#x).n by A1,A34,A43,A39,A44,Th27;
end;
dom F1 = (the carrier of S) by PARTFUN1:def 2;
then
A45: rng the_arity_of o c= dom F1;
commute (H#x) in Funcs (I,Funcs (dom(the_arity_of o),D)) by A27,A32,
FUNCT_6:55;
then consider ff be Function such that
A46: ff = commute (H#x) and
A47: dom ff = I and
A48: rng ff c= Funcs (dom(the_arity_of o),D) by FUNCT_2:def 2;
ff.ii in rng ff by A47,FUNCT_1:def 3;
then
A49: ex gg be Function st gg = (commute (H#x)).ii & dom gg = dom(
the_arity_of o) & rng gg c= D by A46,A48,FUNCT_2:def 2;
A50: x in product doms (F1*the_arity_of o) by Th12;
dom (F1#x) = dom ((Frege(F1*the_arity_of o)).x) by MSUALG_3:def 5
.= dom ((F1*the_arity_of o)..x) by A50,PRALG_2:def 2
.= dom (F1*the_arity_of o) /\ dom x by PRALG_1:def 19
.= dom (the_arity_of o) /\ dom x by A45,RELAT_1:27
.= dom the_arity_of o by A42;
then F1#x = (commute (H#x)).ii by A49,A37;
then f.i9 = Den(o,A.ii).((commute (H#x)).ii) by A1,A17,A34,A36,Th27
.= f1.i9 by A27,Th22;
hence f.i9 = f1.i9;
end;
(commute ((commute F).s9)).(Den(o,U1).x) in product(Carrier(A,s9)
) by A1,A17,Th28;
then dom f = I by PARTFUN1:def 2;
then (commute ((commute F).s9)).(Den(o,U1).x) = f1 by A31,A33;
hence thesis by A2;
end;
end;
end;
take H;
for i be Element of I holds proj(A,i) ** H = F.i
proof
let i be Element of I;
consider F1 be ManySortedFunction of U1,A.i such that
A51: F1 = F.i and
F1 is_homomorphism U1,A.i by A1;
A52: dom(proj(A,i) ** H) = (dom proj(A,i)) /\ (dom H) by PBOOLE:def 19
.= CA /\ (dom H) by PARTFUN1:def 2
.= CA /\ CA by PARTFUN1:def 2
.= CA;
A53: now
let s9 be object;
assume s9 in CA;
then reconsider s1 = s9 as SortSymbol of S;
A54: (proj(A,i) ** H).s9 = (proj(A,i).s1)*(H.s1) by A52,PBOOLE:def 19
.= (proj (Carrier(A,s1),i)) * (H.s1) by Def2
.= ((proj (Carrier(A,s1),i))) * (commute (commute F).s1) by A2;
(commute F).s1 in Funcs (I,Funcs(SU.s1,SA)) by A1,Th26;
then commute ((commute F).s1) in Funcs (SU.s1,Funcs(I,SA)) by FUNCT_6:55;
then consider f9 be Function such that
A55: f9 = (commute (commute F).s1) and
A56: dom f9 = SU.s1 and
rng f9 c= Funcs(I,SA) by FUNCT_2:def 2;
rng f9 c= dom (proj (Carrier(A,s1),i))
proof
let y be object;
assume y in rng f9;
then consider x9 be object such that
A57: x9 in dom f9 and
A58: f9.x9 = y by FUNCT_1:def 3;
(commute (commute F).s1).x9 in product (Carrier(A,s1)) by A1,A56,A57
,Th28;
hence thesis by A55,A58,CARD_3:def 16;
end;
then
A59: dom ((proj(A,i) ** H).s9) = SU.s9 by A55,A56,A54,RELAT_1:27;
A60: now
let x be object;
assume
A61: x in SU.s9;
then ((commute (commute F).s1).x) in product (Carrier(A,s1)) by A1,Th28
;
then
A62: ((commute (commute F).s1).x) in dom (proj (Carrier(A,s1),i )) by
CARD_3:def 16;
thus ((proj(A,i) ** H).s9).x = (proj (Carrier(A,s1),i)).((commute (
commute F).s1).x) by A54,A59,A61,FUNCT_1:12
.= ((commute (commute F).s1).x).i by A62,CARD_3:def 16
.= F1.s9.x by A1,A51,A61,Th27;
end;
dom (F1.s9) = dom (F1.s1) .= SU.s9 by FUNCT_2:def 1;
hence (proj(A,i) ** H).s9 = F1.s9 by A59,A60;
end;
dom F1 = CA by PARTFUN1:def 2;
hence thesis by A51,A52,A53;
end;
hence thesis by A16;
end;
begin :: The Class of Family of Many Sorted Algebras
definition
let I,J,S;
mode MSAlgebra-Class of S,J -> ManySortedSet of I means
:Def3:
for i be set st i in I holds it.i is MSAlgebra-Family of J.i,S;
existence
proof
defpred P[object,object] means $2 is MSAlgebra-Family of J.$1,S;
A1: for i be object st i in I ex F be object st P[i,F]
proof
let i be object such that
i in I;
set F = the MSAlgebra-Family of J.i,S;
take F;
thus thesis;
end;
consider C be ManySortedSet of I such that
A2: for i be object st i in I holds P[i,C.i] from PBOOLE:sch 3(A1);
take C;
thus thesis by A2;
end;
end;
definition
let I,S,A,EqR;
func A / EqR -> MSAlgebra-Class of S,id Class EqR means
:Def4:
for c st c in Class EqR holds it.c = A|c;
existence
proof
thus ex X be MSAlgebra-Class of S,id Class EqR st for c st c in Class EqR
holds X.c = A|c
proof
deffunc F(set) = A|$1;
consider X be ManySortedSet of Class EqR such that
A1: for c st c in Class EqR holds X.c = F(c) from PBOOLE:sch 7;
X is MSAlgebra-Class of S,id Class EqR
proof
let c be set;
assume
A2: c in Class EqR;
A3: dom (A|c) = (dom A) /\ c by RELAT_1:61
.= I /\ c by PARTFUN1:def 2
.= c by A2,XBOOLE_1:28
.= (id Class EqR).c by A2,FUNCT_1:18;
then reconsider ac = A|c as ManySortedSet of (id Class EqR).c by
PARTFUN1:def 2,RELAT_1:def 18;
ac is MSAlgebra-Family of (id Class EqR).c,S
proof
let i be object;
assume
A4: i in (id Class EqR).c;
dom ac = c by A2,A3,FUNCT_1:18;
then reconsider i9 = i as Element of I by A2,A3,A4;
A.i9 is non-empty MSAlgebra over S;
hence thesis by A3,A4,FUNCT_1:47;
end;
hence thesis by A1,A2;
end;
then reconsider X as MSAlgebra-Class of S,id Class EqR;
take X;
thus thesis by A1;
end;
end;
uniqueness
proof
for X, Y be MSAlgebra-Class of S,id Class EqR st (for c st c in Class
EqR holds X.c = A|c) & for c st c in Class EqR holds Y.c = A|c holds X = Y
proof
let X, Y be MSAlgebra-Class of S,id Class EqR such that
A5: for c st c in Class EqR holds X.c = A|c and
A6: for c st c in Class EqR holds Y.c = A|c;
now
let c be object;
assume
A7: c in Class EqR;
reconsider cc = c as set by TARSKI:1;
thus X.c = A|cc by A5,A7
.= Y.c by A6,A7;
end;
hence thesis;
end;
hence thesis;
end;
end;
definition
let I,S;
let J be non-empty ManySortedSet of I;
let C be MSAlgebra-Class of S,J;
func product C -> MSAlgebra-Family of I,S means
:Def5:
for i st i in I ex Ji
be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & it.i
= product Cs;
existence
proof
thus ex PC be MSAlgebra-Family of I,S st for i st i in I ex Ji be non
empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & PC.i =
product Cs
proof
defpred P[object,object] means
ex Ji be non empty set, Cs be MSAlgebra-Family
of Ji,S st Ji = J.$1 & Cs = C.$1 & $2 = product Cs;
A1: now
let i be object;
assume
A2: i in I;
then reconsider Ji = J.i as non empty set;
reconsider Cs = C.i as MSAlgebra-Family of Ji,S by A2,Def3;
ex a be object st a = product Cs;
then consider j be object such that
A3: ex Ji be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji =
J.i & Cs = C.i & j = product Cs;
reconsider j as object;
take j;
thus P[i,j] by A3;
end;
consider PC be ManySortedSet of I such that
A4: for i be object st i in I holds P[i,PC.i] from PBOOLE:sch 3(A1);
now
let i be object;
assume i in I;
then
ex Ji be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.i
& Cs = C.i & PC.i = product Cs by A4;
hence PC.i is non-empty MSAlgebra over S;
end;
then reconsider PC as MSAlgebra-Family of I,S by PRALG_2:def 5;
take PC;
thus thesis by A4;
end;
end;
uniqueness
proof
for PC1,PC2 be MSAlgebra-Family of I,S st (for i st i in I ex Ji be
non empty set , Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & PC1.i =
product Cs ) & for i st i in I ex Ji be non empty set , Cs be MSAlgebra-Family
of Ji,S st Ji =J.i & Cs = C.i & PC2.i = product Cs holds PC1 = PC2
proof
let PC1,PC2 be MSAlgebra-Family of I,S such that
A5: ( for i st i in I ex Ji be non empty set , Cs be
MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & PC1.i = product Cs)& for i st
i in I ex Ji be non empty set , Cs be MSAlgebra-Family of Ji,S st Ji =J.i & Cs
= C.i & PC2.i = product Cs;
now
let i1 be object;
assume i1 in I;
then reconsider i9 = i1 as Element of I;
(ex Ji1 be non empty set, Cs1 be MSAlgebra-Family of Ji1,S st Ji1
= J.i9 & Cs1 = C.i9 & PC1.i9 = product Cs1 )& ex Ji2 be non empty set, Cs2 be
MSAlgebra-Family of Ji2,S st Ji2 = J.i9 & Cs2 = C.i9 & PC2.i9 = product Cs2 by
A5;
hence PC1.i1 = PC2.i1;
end;
hence thesis;
end;
hence thesis;
end;
end;
theorem
for A be MSAlgebra-Family of I,S, EqR be Equivalence_Relation of I
holds product A, product (product (A/EqR)) are_isomorphic
proof
let A be MSAlgebra-Family of I,S, EqR be Equivalence_Relation of I;
set U1 = product A, U2 = product product (A/EqR);
set U19 = the Sorts of U1, U29 = the Sorts of U2;
defpred P[object,object,object] means
for f1,g1 being Function st f1 = $2 & g1 = $1
for e being Element of Class EqR holds g1.e = f1|e;
A1: for s be object st s in the carrier of S
for x be object st x in U19.s ex y be object st y in U29.s & P[y,x,s]
proof
let s be object;
assume s in the carrier of S;
then reconsider s9 = s as SortSymbol of S;
A2: U19.s9 = product Carrier(A,s9) by PRALG_2:def 10;
let x be object such that
A3: x in U19.s;
reconsider x as Function by A3,A2;
deffunc F(set) = x|$1;
consider y being ManySortedSet of Class EqR such that
A4: for c st c in Class EqR holds y.c = F(c) from PBOOLE:sch 7;
A5: dom Carrier(product (A/EqR),s9) = Class EqR by PARTFUN1:def 2;
A6: for a be object st a in dom (Carrier(product (A/EqR),s9)) holds y.a in (
Carrier(product (A/EqR),s9)).a
proof
set A9 = product (A/EqR);
let a be object such that
A7: a in dom (Carrier(product (A/EqR),s9));
reconsider a as set by TARSKI:1;
A8: (A/EqR).a = A|a by A7,Def4;
reconsider a as non empty Subset of I by A5,A7;
A9: ex U0 being MSAlgebra over S st U0 = A9.a & (Carrier(A9, s9)).a = (
the Sorts of U0).s9 by A7,PRALG_2:def 9;
A10: dom (A|a) = dom A /\ a by RELAT_1:61
.= I /\ a by PARTFUN1:def 2
.= a by XBOOLE_1:28;
then reconsider Aa1 = A|a as ManySortedSet of a by PARTFUN1:def 2;
for i be object st i in a holds Aa1.i is non-empty MSAlgebra over S
proof
let i be object;
assume
A11: i in a;
then A.i is non-empty MSAlgebra over S by PRALG_2:def 5;
hence thesis by A10,A11,FUNCT_1:47;
end;
then reconsider Aa = Aa1 as MSAlgebra-Family of a,S by PRALG_2:def 5;
x|a in product((Carrier(A,s9))|a) by A3,A2,Th1;
then
A12: x|a in product (Carrier(Aa,s9)) by Th2;
consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such that
A13: Ji = (id Class EqR).a and
A14: Cs = (A/EqR).a & A9.a = product Cs by A7,Def5;
Ji = a by A7,A13,FUNCT_1:18;
then (Carrier(A9,s9)).a = product (Carrier(Aa,s9)) by A8,A14,A9,
PRALG_2:def 10;
hence thesis by A4,A7,A12;
end;
take y;
dom Carrier(product (A/EqR),s9) = Class EqR by PARTFUN1:def 2
.= dom y by PARTFUN1:def 2;
then y in product Carrier(product (A/EqR),s9) by A6,CARD_3:9;
hence thesis by A4,PRALG_2:def 10;
end;
consider F be ManySortedFunction of U19, U29 such that
A15: for s be object st s in the carrier of S
ex f be Function of U19
.s, U29.s st f = F.s & for x be object st x in U19.s holds P[f.x,x,s]
from
MSSUBFAM:sch 1(A1);
A16: F is_homomorphism U1,U2
proof
let o be OperSymbol of S such that
Args(o,U1) <> {};
let x be Element of Args(o,U1);
thus (F.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,U2).(F#x)
proof
A17: Den(o,U1).x in Result(o,U1);
then
A18: Den(o,U1).x in U19.(the_result_sort_of o) by PRALG_2:3;
set s = the_result_sort_of o, U3 = product (A/EqR);
A19: U29.s = product Carrier(U3,s) by PRALG_2:def 10;
A20: ex f be Function of U19.s, U29.s st f = F.s &
for x9 be object st x9 in
U19.s holds P[f.x9,x9,s] by A15;
A21: dom (F.s) = (SORTS A).s by FUNCT_2:def 1
.= product Carrier(A,s) by PRALG_2:def 10;
A22: Den(o,U1).x in product Carrier(A,s) by Th19;
per cases;
suppose
A23: the_arity_of o = {};
then Args(o,U1) = {{}} by PRALG_2:4;
then
A24: x = {} by TARSKI:def 1;
then
A25: F.s.const(o,U1) in rng (F.s) by A21,A22,FUNCT_1:def 3;
reconsider g1 = F.s.const(o,U1) as Function by A19;
A26: dom (const(o,U1)) = I by PARTFUN1:def 2,A22,A24;
A27: now
let e be Element of Class EqR;
consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such
that
A28: Ji = (id Class EqR).e and
A29: Cs = (A/EqR).e and
A30: U3.e = product Cs by Def5;
A31: dom (const(o,product A)|e) = I /\ e by A26,RELAT_1:61
.= e by XBOOLE_1:28;
A32: now
let i1 be object;
A33: dom(A|e) = dom A /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def 2
.= e by XBOOLE_1:28;
assume
A34: i1 in e;
then reconsider ii = i1 as Element of Ji by A28;
reconsider ii9 = ii as Element of I by A34;
Cs = A|e by A29,Def4;
then
A35: Cs.ii = A.ii9 by A34,A33,FUNCT_1:47;
thus (const(o,product A)|e).i1 = const(o,product A).i1 by A31,A34,
FUNCT_1:47
.= const(o,A.ii9) by A23,Th9
.= const(o,product Cs).i1 by A23,A35,Th9;
end;
const(o,product Cs) in Funcs(Ji, union the set of all
Result(o,Cs.i9) where
i9 is Element of Ji) by A23,Th8;
then dom (const(o,product Cs)) = e by A28,FUNCT_2:92;
hence const(o,U1)|e = const(o,U3.e) by A30,A31,A32,FUNCT_1:2;
end;
A36: const(o,U1) in U19.(the_result_sort_of o) by A17,A24,PRALG_2:3;
A37: now
let x1 be object;
consider f1 be Function such that
A38: f1 = const(o,U1);
assume x1 in Class EqR;
then reconsider e = x1 as Element of Class EqR;
g1.e = f1|e by A20,A36,A38;
hence g1.x1 = const(o,U3.e) by A27,A38
.= const(o,product U3).x1 by A23,Th9;
end;
const(o,U2) in Funcs(Class EqR, union the set of all
Result(o,U3.i9) where i9
is Element of Class EqR) by A23,Th8;
then
A39: dom const(o,U2) = Class EqR by FUNCT_2:92;
dom g1 = Class EqR by PARTFUN1:def 2,A19,A25;
then F.s.const(o,U1) = const(o,U2) by A39,A37,FUNCT_1:2;
hence thesis by A23,A24,Th11;
end;
suppose
A40: the_arity_of o <> {};
A41: Den(o,U2).(F#x) in product Carrier(U3,s) by Th19;
then reconsider f1 = Den(o,U2).(F#x) as Function;
A42: dom f1 = Class EqR by PARTFUN1:def 2,A41;
A43: (F.s).(Den(o,U1).x) in rng (F.s) by A21,A22,FUNCT_1:def 3;
reconsider g1 = (F.s).(Den(o,U1).x) as Function by A19;
A44: now
let e be Element of Class EqR;
consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such
that
A45: Ji = (id Class EqR).e and
A46: Cs = (A/EqR).e and
A47: U3.e = product Cs by Def5;
A48: (commute (F#x)).e is Element of Args(o,U3.e) by A40,Th20;
then
A49: Den (o,U3.e).((commute (F#x)).e) in product Carrier(Cs,s) by A47,Th19
;
then reconsider f3 = Den(o,U3.e).((commute (F#x)).e) as Function;
A50: now
let i1 be Element of I;
assume
A51: i1 in e;
then reconsider i2 = i1 as Element of Ji by A45;
A52: now
let n be object;
assume
A53: n in dom (the_arity_of o);
then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 3;
then reconsider s1 = (the_arity_of o).n as SortSymbol of S;
A54: x.n in product Carrier(A,(the_arity_of o)/.n) by A53,Th15;
then reconsider f4 = x.n as Function;
A55: x.n in product Carrier(A,s1) by A53,A54,PARTFUN1:def 6;
then
A56: x.n in (SORTS A).s1 by PRALG_2:def 10;
dom f4 = I by PARTFUN1:def 2,A55; then
A57: dom (f4|e) = I /\ e by RELAT_1:61
.= e by XBOOLE_1:28;
(F#x).n in product Carrier (U3,(the_arity_of o)/.n) by A53,Th15;
then reconsider f5 = (F#x).n as Function;
consider f7 be Function of U19.s1, U29.s1 such that
A58: f7 = F.s1 and
A59: for x9 be object st x9 in U19.s1 holds P[f7.x9,x9,s1] by A15;
f5 = F.((the_arity_of o)/.n).(x.n) by A53,Th13
.= f7.(x.n) by A53,A58,PARTFUN1:def 6;
then
A60: f5.e = f4|e by A56,A59;
then reconsider f6 = f5.e as Function;
f6 = ((commute (F#x)).e).n by A53,Th21;
hence
((commute((commute (F#x)).e)).i1).n = (f4|e).i2 by A47,A48,A53
,A60,Th21
.= f4.i2 by A51,A57,FUNCT_1:47
.= ((commute x).i1).n by A53,Th21;
end;
(commute x).i1 is Element of Args(o,A.i1) by A40,Th20;
then (commute x).i1 in Args(o,A.i1);
then (commute x).i1 in product ((the Sorts of A.i1)*(the_arity_of
o)) by PRALG_2:3;
then
A61: dom ((commute x).i1) = dom ((the Sorts of A.i1)*(the_arity_of
o)) by CARD_3:9
.= dom (the_arity_of o) by PRALG_2:3;
(commute ((commute (F#x)).e)).i2 is Element of Args(o,Cs.i2)
by A40,A47,A48,Th20;
then (commute ((commute (F#x)).e)).i2 in Args(o,Cs.i2);
then
(commute ((commute (F#x)).e)).i2 in product ((the Sorts of Cs
.i2)*(the_arity_of o)) by PRALG_2:3;
then dom ((commute ((commute (F#x)).e)).i1) = dom ((the Sorts of
Cs.i2)*(the_arity_of o)) by CARD_3:9
.= dom (the_arity_of o) by PRALG_2:3;
hence ((commute ((commute (F#x)).e)).i1) = ((commute x).i1) by A61
,A52;
end;
let f2 be Function such that
A62: f2 = Den(o,U1).x;
dom f2 = I by PARTFUN1:def 2,A22,A62;
then
A63: dom (f2|e) = I /\ e by RELAT_1:61
.= e by XBOOLE_1:28;
A64: (commute (F#x)).e is Element of Args(o,product Cs) by A40,A47,Th20;
A65: now
let x1 be object;
A66: dom(A|e) = dom A /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def 2
.= e by XBOOLE_1:28;
assume
A67: x1 in e;
then reconsider i2 = x1 as Element of Ji by A45;
reconsider i1 = i2 as Element of I by A67;
Cs = A|e by A46,Def4;
then Cs.i2 = A.i1 by A67,A66,FUNCT_1:47;
hence
f3.x1 = Den(o,A.i1).((commute ((commute (F#x)).e)).i2) by A40,A47
,A64,Th22
.= Den(o,A.i1).((commute x).i1) by A50,A67
.= f2.x1 by A40,A62,Th22
.= (f2|e).x1 by A63,A67,FUNCT_1:47;
end;
dom f3 = dom (Carrier(Cs,s)) by A49,CARD_3:9
.= e by A45,PARTFUN1:def 2;
hence f2|e = Den(o,U3.e).((commute (F#x)).e) by A63,A65,FUNCT_1:2;
end;
A68: now
reconsider f2 = Den(o,U1).x as Function by A22;
let x1 be object;
assume x1 in Class EqR;
then reconsider e = x1 as Element of Class EqR;
g1.e = f2|e by A20,A18;
hence g1.x1 = Den(o,U3.e).((commute (F#x)).e) by A44
.= f1.x1 by A40,Th22;
end;
dom g1 = Class EqR by PARTFUN1:def 2,A19,A43;
hence thesis by A42,A68,FUNCT_1:2;
end;
end;
end;
F is "1-1"
proof
let s be set, g be Function such that
A69: s in dom F and
A70: F.s = g;
consider f being Function of U19.s, U29.s such that
A71: f = F.s and
A72: for x be object st x in U19.s holds P[f.x,x,s] by A15,A69;
let x1,x2 be object such that
A73: x1 in dom g and
A74: x2 in dom g and
A75: g.x1 = g.x2;
A76: dom f = dom g by A70,A71;
thus x1 = x2
proof
reconsider s9 = s as SortSymbol of S by A69;
A77: U19.s9 = product Carrier(A,s9) by PRALG_2:def 10;
then
A78: ex gg be Function st x1 = gg & dom gg = dom Carrier(A,s9 ) &
for x9 be object st x9 in dom Carrier(A,s9) holds gg.x9 in (Carrier(A,s9)).x9
by A73,A76,
CARD_3:def 5;
A79: ex gg1 be Function st x2 = gg1 & dom gg1 = dom Carrier(A,s9) & for
x9 be object st x9 in dom Carrier(A,s9) holds gg1.x9 in (Carrier(A,s9) ).x9
by A74
,A76,A77,CARD_3:def 5;
reconsider x2 as Function by A74,A76,A77;
A80: dom x2 = I by A79,PARTFUN1:def 2;
reconsider x1 as Function by A73,A76,A77;
A81: U29.s = product Carrier(product (A/EqR),s9) by PRALG_2:def 10;
A82: for i be object st i in I holds x1.i = x2.i
proof
reconsider f99 = f.x2 as Function by A81;
let i be object;
assume
A83: i in I;
then
A84: Class(EqR,i) is Element of Class EqR by EQREL_1:def 3;
then x1|(Class(EqR,i)) = f99.(Class(EqR,i)) by A70,A73,A75,A71,A72,A76
.= x2|(Class(EqR,i)) by A74,A72,A76,A84;
then x1.i = (x2|(Class(EqR,i))).i by A83,EQREL_1:20,FUNCT_1:49
.= x2.i by A83,EQREL_1:20,FUNCT_1:49;
hence thesis;
end;
dom x1 = I by A78,PARTFUN1:def 2;
hence thesis by A80,A82,FUNCT_1:2;
end;
end;
then
A85: F is_monomorphism U1,U2 by A16;
F is "onto"
proof
let s be set such that
A86: s in the carrier of S;
reconsider s9 = s as SortSymbol of S by A86;
consider f be Function of U19.s, U29.s such that
A87: f = F.s and
A88: for x be object st x in U19.s holds P[f.x,x,s] by A15,A86;
A89: U19.s9 = product Carrier(A,s9) by PRALG_2:def 10;
for y be object holds y in (U29.s) iff
ex x be object st x in dom f & y = f.x
proof
let y be object;
A90: y in U29.s implies ex x be set st x in dom f & y = f.x
proof
assume y in (U29.s);
then
A91: y in product Carrier(product (A/EqR),s9) by PRALG_2:def 10;
then
A92: ex gg be Function st y = gg & dom gg = dom (Carrier( product (A/
EqR),s9)) & for x9 be object st x9 in dom (Carrier(product (A/EqR),s9) )
holds gg.
x9 in (Carrier(product (A/EqR),s9)).x9 by CARD_3:def 5;
reconsider y as Function by A91;
defpred Q[object,object] means
ex e being Element of Class EqR, f being
Function st $1 in e & f = y.e & $2 = f.$1;
A93: for i be object st i in I ex j being object st Q[i,j]
proof
let i be object such that
A94: i in I;
Class(EqR,i) in Class EqR by A94,EQREL_1:def 3;
then consider e be Element of Class EqR such that
A95: e = Class(EqR,i);
consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such
that
Ji = (id Class EqR).e and
Cs = (A/EqR).e and
A96: (product (A/EqR)).e = product Cs by Def5;
ex U0 being MSAlgebra over S st U0 = (product (A/EqR)).e & (
Carrier(product (A/EqR),s9)).e = (the Sorts of U0).s9 by PRALG_2:def 9;
then dom (Carrier(product (A/EqR),s9)) = Class EqR & (Carrier(
product (A/EqR),s9) ).e = product Carrier(Cs,s9) by A96,PARTFUN1:def 2
,PRALG_2:def 10;
then reconsider y9 = y.e as Function by A92,Lm1;
Q[i,y9.i] by A94,A95,EQREL_1:20;
hence thesis;
end;
consider x being ManySortedSet of I such that
A97: for i be object st i in I holds Q[i,x.i] from PBOOLE:sch 3(A93
);
A98: dom Carrier(product (A/EqR),s9) = Class EqR by PARTFUN1:def 2;
A99: for z be object st z in dom Carrier(A,s9)
holds x.z in (Carrier(A, s9)).z
proof
let z be object;
assume z in dom Carrier(A,s9);
then z in I;
then consider
e being Element of Class EqR,f1 being Function such that
A100: z in e and
A101: f1 = y.e & x.z = f1.z by A97;
dom ((Carrier(A,s9))|e) = dom Carrier(A,s9) /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def 2
.= e by XBOOLE_1:28;
then
A102: ((Carrier(A,s9))|e).z = (Carrier(A,s9)).z by A100,FUNCT_1:47;
consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such
that
A103: Ji = (id Class EqR).e and
A104: Cs = (A/EqR).e and
A105: (product (A/EqR)).e = product Cs by Def5;
Cs = A|e & Ji = e by A103,A104,Def4;
then
A106: Carrier(Cs,s9) = (Carrier(A,s9))|e by Th2;
ex U0 being MSAlgebra over S st U0 = (product (A/EqR)).e & (
Carrier(product (A/EqR),s9)).e = (the Sorts of U0).s9 by PRALG_2:def 9;
then
A107: (Carrier(product (A/EqR),s9)).e = product Carrier(Cs,s9) by A105,
PRALG_2:def 10;
y.e in (Carrier(product (A/EqR),s9)).e by A92,A98;
then
A108: ex g be Function st y.e = g & dom g = dom Carrier(Cs,s9) & for
x9 be object st x9 in dom Carrier(Cs,s9) holds g.x9 in (Carrier(Cs,s9)).x9
by A107
,CARD_3:def 5;
dom Carrier(Cs,s9) = e by A103,PARTFUN1:def 2;
hence thesis by A100,A101,A108,A102,A106;
end;
dom x = I by PARTFUN1:def 2
.= dom Carrier(A,s9) by PARTFUN1:def 2;
then
A109: x in U19.s9 by A89,A99,CARD_3:9;
then
A110: x in dom f by FUNCT_2:def 1;
then f.x in rng f by FUNCT_1:def 3;
then f.x in U29.s;
then
A111: f.x in product Carrier(product (A/EqR),s9) by PRALG_2:def 10;
then reconsider f9 = f.x as Function;
A112: for e be object st e in Class EqR holds y.e = f9.e
proof
let e be object;
assume e in Class EqR;
then reconsider e as Element of Class EqR;
consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such
that
A113: Ji = (id Class EqR).e and
Cs = (A/EqR).e and
A114: (product (A/EqR)).e = product Cs by Def5;
ex U0 being MSAlgebra over S st U0 = (product (A/EqR)).e & (
Carrier(product (A/EqR),s9)).e = (the Sorts of U0).s9 by PRALG_2:def 9;
then
A115: (Carrier(product (A/EqR),s9)).e = product Carrier(Cs,s9) by A114,
PRALG_2:def 10;
A116: y.e in (Carrier(product (A/EqR),s9)).e by A92,A98;
then reconsider y9 = y.e as Function by A115;
A117: dom (x|e) = dom x /\ e by RELAT_1:61
.= I /\ e by PARTFUN1:def 2
.= e by XBOOLE_1:28;
A118: for i be object st i in e holds (x|e).i = y9.i
proof
let i be object;
assume
A119: i in e;
then consider
e1 being Element of Class EqR,f1 being Function such that
A120: i in e1 and
A121: f1 = y.e1 & x.i = f1.i by A97;
e = e1 by A119,A120,Th3;
hence thesis by A117,A119,A121,FUNCT_1:47;
end;
ex g be Function st y.e = g & dom g = dom Carrier(Cs,s9) &
for x9 be object st x9 in dom Carrier(Cs,s9) holds
g.x9 in (Carrier(Cs,s9)).x9 by A116,A115,CARD_3:def 5;
then dom y9 = e by A113,PARTFUN1:def 2;
then x|e = y9 by A117,A118;
hence thesis by A88,A109;
end;
ex gg9 be Function st f.x = gg9 & dom gg9 = dom (Carrier (product
(A/EqR),s9)) &
for x9 be object st x9 in dom (Carrier(product (A/EqR),s9 )) holds
gg9.x9 in (Carrier(product (A/EqR),s9)).x9 by A111,CARD_3:def 5;
then y = f9 by A92,A112;
hence thesis by A110;
end;
(ex x be set st x in dom f & y = f.x) implies y in (U29.s)
proof
given x be set such that
A122: x in dom f and
A123: y = f.x;
f.x in rng f by A122,FUNCT_1:def 3;
hence thesis by A123;
end;
hence y in (U29.s) iff ex x be object st x in dom f & y = f.x by A90;
end;
hence thesis by A87,FUNCT_1:def 3;
end;
then F is_epimorphism U1,U2 by A16;
then F is_isomorphism U1,U2 by A85;
hence thesis;
end;