:: MSALIMIT semantic presentation

begin


registration
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let AF be MSAlgebra-Family of I,S;
let i be Element of I;
let o be OperSymbol of S;
cluster((OPER AF) . i) . o ->  Relation-like Function-like ;
coherence
 ( ((OPER AF) . i) . o is Function-like & ((OPER AF) . i) . o is Relation-like )
proof
 ex U0 being MSAlgebra over S st
( U0 = AF . i & (OPER AF) . i = the Charact of U0 ) by PRALG_2:def_11;
hence  ( ((OPER AF) . i) . o is Function-like & ((OPER AF) . i) . o is Relation-like ) ; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let AF be MSAlgebra-Family of I,S;
let s be SortSymbol of S;
cluster(SORTS AF) . s ->  functional ;
coherence
 (SORTS AF) . s is functional
proof
 (SORTS AF) . s = product (Carrier (AF,s)) by PRALG_2:def_10;
hence  (SORTS AF) . s is functional ; ::_thesis: verum
end;
end;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
mode OrderedAlgFam of P,S ->  MSAlgebra-Family of the carrier of P,S means :Def1: :: MSALIMIT:def 1
 ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (it . i),(it . j) ex f2 being ManySortedFunction of (it . j),(it . k) st
( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism it . i,it . j );
existence
 ex b1 being MSAlgebra-Family of the carrier of P,S ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (b1 . i),(b1 . j) ex f2 being ManySortedFunction of (b1 . j),(b1 . k) st
( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism b1 . i,b1 . j )
proof
reconsider T1 = the InternalRel of P as Relation of the carrier of P ;
set A = the non-empty MSAlgebra over S;
reconsider Z = the carrier of P --> the non-empty MSAlgebra over S as ManySortedSet of the carrier of P ;
 for i being set st i in the carrier of P holds
Z . i is non-empty MSAlgebra over S by FUNCOP_1:7;
then reconsider Z = Z as MSAlgebra-Family of the carrier of P,S by PRALG_2:def_5;
take  Z ; ::_thesis: ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (Z . i),(Z . j) ex f2 being ManySortedFunction of (Z . j),(Z . k) st
( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism Z . i,Z . j )
set G = the InternalRel of P --> (id the Sorts of the non-empty MSAlgebra over S);
reconsider G = the InternalRel of P --> (id the Sorts of the non-empty MSAlgebra over S) as ManySortedFunction of the InternalRel of P ;
take  G ; ::_thesis: for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (Z . i),(Z . j) ex f2 being ManySortedFunction of (Z . j),(Z . k) st
( f1 = G . (j,i) & f2 = G . (k,j) & G . (k,i) = f2 ** f1 & f1 is_homomorphism Z . i,Z . j )
let i, j, k be Element of P; ::_thesis: ( i >= j & j >= k implies ex f1 being ManySortedFunction of (Z . i),(Z . j) ex f2 being ManySortedFunction of (Z . j),(Z . k) st
( f1 = G . (j,i) & f2 = G . (k,j) & G . (k,i) = f2 ** f1 & f1 is_homomorphism Z . i,Z . j ) )
A1: Z . j = the non-empty MSAlgebra over S by FUNCOP_1:7;
 Z . k = the non-empty MSAlgebra over S by FUNCOP_1:7;
then consider F2 being ManySortedFunction of (Z . j),(Z . k) such that
A2: F2 = id the Sorts of the non-empty MSAlgebra over S by A1;
assume  ( i >= j & j >= k ) ; ::_thesis: ex f1 being ManySortedFunction of (Z . i),(Z . j) ex f2 being ManySortedFunction of (Z . j),(Z . k) st
( f1 = G . (j,i) & f2 = G . (k,j) & G . (k,i) = f2 ** f1 & f1 is_homomorphism Z . i,Z . j )
then A3: ( [j,i] in the InternalRel of P & [k,j] in the InternalRel of P ) by ORDERS_2:def_5;
 field T1 = the carrier of P by ORDERS_1:12;
then  T1 is_transitive_in the carrier of P by RELAT_2:def_16;
then A4: [k,i] in T1 by A3, RELAT_2:def_8;
A5: Z . i = the non-empty MSAlgebra over S by FUNCOP_1:7;
then consider F1 being ManySortedFunction of (Z . i),(Z . j) such that
A6: F1 = id the Sorts of the non-empty MSAlgebra over S by A1;
take  F1 ; ::_thesis: ex f2 being ManySortedFunction of (Z . j),(Z . k) st
( F1 = G . (j,i) & f2 = G . (k,j) & G . (k,i) = f2 ** F1 & F1 is_homomorphism Z . i,Z . j )
take  F2 ; ::_thesis: ( F1 = G . (j,i) & F2 = G . (k,j) & G . (k,i) = F2 ** F1 & F1 is_homomorphism Z . i,Z . j )
 F2 ** F1 = id the Sorts of the non-empty MSAlgebra over S by A6, A2, MSUALG_3:3;
hence  ( F1 = G . (j,i) & F2 = G . (k,j) & G . (k,i) = F2 ** F1 & F1 is_homomorphism Z . i,Z . j ) by A3, A5, A1, A6, A2, A4, FUNCOP_1:7, MSUALG_3:9; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines OrderedAlgFam MSALIMIT:def_1_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for b3 being MSAlgebra-Family of the carrier of P,S holds
( b3 is OrderedAlgFam of P,S iff ex F being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (b3 . i),(b3 . j) ex f2 being ManySortedFunction of (b3 . j),(b3 . k) st
( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism b3 . i,b3 . j ) );

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
mode Binding of OAF ->  ManySortedFunction of the InternalRel of P means :Def2: :: MSALIMIT:def 2
 for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = it . (j,i) & f2 = it . (k,j) & it . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j );
existence
 ex b1 being ManySortedFunction of the InternalRel of P st
for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = b1 . (j,i) & f2 = b1 . (k,j) & b1 . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by Def1;
end;

:: deftheorem Def2 defines Binding MSALIMIT:def_2_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for b4 being ManySortedFunction of the InternalRel of P holds
( b4 is Binding of OAF iff for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = b4 . (j,i) & f2 = b4 . (k,j) & b4 . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) );

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
let i, j be Element of P;
assume A1: i >= j ;
func bind (B,i,j) ->  ManySortedFunction of (OAF . i),(OAF . j) equals :Def3: :: MSALIMIT:def 3
B . (j,i);
coherence
 B . (j,i) is ManySortedFunction of (OAF . i),(OAF . j)
proof
 j >= j by ORDERS_2:1;
then  ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . j) st
( f1 = B . (j,i) & f2 = B . (j,j) & B . (j,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by A1, Def2;
hence  B . (j,i) is ManySortedFunction of (OAF . i),(OAF . j) ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines bind MSALIMIT:def_3_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j holds
bind (B,i,j) = B . (j,i);

theorem Th1: :: MSALIMIT:1
for P being non empty Poset
for i, j, k being Element of P
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF st i >= j & j >= k holds
(bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k)
proof
let P be non empty Poset; ::_thesis: for i, j, k being Element of P
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF st i >= j & j >= k holds
(bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k)
let i, j, k be Element of P; ::_thesis: for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF st i >= j & j >= k holds
(bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k)
let S be non empty non void ManySortedSign ; ::_thesis: for OAF being OrderedAlgFam of P,S
for B being Binding of OAF st i >= j & j >= k holds
(bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k)
let OAF be OrderedAlgFam of P,S; ::_thesis: for B being Binding of OAF st i >= j & j >= k holds
(bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k)
let B be Binding of OAF; ::_thesis: ( i >= j & j >= k implies (bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k) )
assume A1: ( i >= j & j >= k ) ; ::_thesis: (bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k)
then A2: ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = B . (j,i) & f2 = B . (k,j) & B . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by Def2;
 ( bind (B,j,k) = B . (k,j) & bind (B,i,j) = B . (j,i) ) by A1, Def3;
hence  (bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k) by A1, A2, Def3, ORDERS_2:3; ::_thesis: verum
end;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let IT be Binding of OAF;
attrIT is normalized  means :Def4: :: MSALIMIT:def 4
 for i being Element of P holds IT . (i,i) = id the Sorts of (OAF . i);
end;

:: deftheorem Def4 defines normalized MSALIMIT:def_4_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for IT being Binding of OAF holds
( IT is normalized iff for i being Element of P holds IT . (i,i) = id the Sorts of (OAF . i) );

theorem Th2: :: MSALIMIT:2
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j holds
for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds
f is_homomorphism OAF . i,OAF . j
proof
let P be non empty Poset; ::_thesis: for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j holds
for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds
f is_homomorphism OAF . i,OAF . j
let S be non empty non void ManySortedSign ; ::_thesis: for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j holds
for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds
f is_homomorphism OAF . i,OAF . j
let OAF be OrderedAlgFam of P,S; ::_thesis: for B being Binding of OAF
for i, j being Element of P st i >= j holds
for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds
f is_homomorphism OAF . i,OAF . j
let B be Binding of OAF; ::_thesis: for i, j being Element of P st i >= j holds
for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds
f is_homomorphism OAF . i,OAF . j
let i, j be Element of P; ::_thesis: ( i >= j implies for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds
f is_homomorphism OAF . i,OAF . j )
assume A1: i >= j ; ::_thesis: for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds
f is_homomorphism OAF . i,OAF . j
let f be ManySortedFunction of (OAF . i),(OAF . j); ::_thesis: ( f = bind (B,i,j) implies f is_homomorphism OAF . i,OAF . j )
assume A2: f = bind (B,i,j) ; ::_thesis: f is_homomorphism OAF . i,OAF . j
 j >= j by ORDERS_2:1;
then  ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . j) st
( f1 = B . (j,i) & f2 = B . (j,j) & B . (j,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by A1, Def2;
hence  f is_homomorphism OAF . i,OAF . j by A1, A2, Def3; ::_thesis: verum
end;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
func Normalized B ->  Binding of OAF means :Def5: :: MSALIMIT:def 5
 for i, j being Element of P st i >= j holds
it . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i))));
existence
 ex b1 being Binding of OAF st
for i, j being Element of P st i >= j holds
b1 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i))))
proof
defpred S1[ set , set ] means  ex i, j being Element of P st
( $1 = [j,i] & $2 = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) );
now__::_thesis:_for_ij_being_set_st_ij_in_the_InternalRel_of_P_holds_
ex_x_being_set_ex_i1,_i2_being_Element_of_P_st_
(_ij_=_[i2,i1]_&_x_=_IFEQ_(i2,i1,(id_the_Sorts_of_(OAF_._i1)),((bind_(B,i1,i2))_**_(id_the_Sorts_of_(OAF_._i1))))_)
let ij be set ; ::_thesis: ( ij in the InternalRel of P implies ex x being set ex i1, i2 being Element of P st
( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) ) )
assume A1: ij in the InternalRel of P ; ::_thesis: ex x being set ex i1, i2 being Element of P st
( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) )
then reconsider i2 = ij `1 , i1 = ij `2 as Element of P by MCART_1:10;
reconsider i1 = i1, i2 = i2 as Element of P ;
deffunc H1( set ) ->  set = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1))));
consider A being ManySortedSet of the InternalRel of P such that
A2: for ij being set st ij in the InternalRel of P holds
A . ij = H1(ij) from PBOOLE:sch_4();
take x = A . ij; ::_thesis: ex i1, i2 being Element of P st
( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) )
take i1 = i1; ::_thesis: ex i2 being Element of P st
( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) )
take i2 = i2; ::_thesis: ( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) )
thus  ( ij = [i2,i1] & x = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) ) by A1, A2, MCART_1:21; ::_thesis: verum
end;
then A3: for z being set st z in the InternalRel of P holds
ex y being set st S1[z,y] ;
consider A being ManySortedSet of the InternalRel of P such that
A4: for ij being set st ij in the InternalRel of P holds
S1[ij,A . ij] from PBOOLE:sch_3(A3);
 for z being set st z in dom A holds
A . z is Function
proof
let z be set ; ::_thesis: ( z in dom A implies A . z is Function )
assume  z in dom A ; ::_thesis: A . z is Function
then  z in the InternalRel of P ;
then consider i1, i2 being Element of P such that
 z = [i2,i1] and
A5: A . z = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) by A4;
percases ( i1 = i2 or i1 <> i2 ) ;
suppose i1 = i2 ; ::_thesis: A . z is Function
hence  A . z is Function by A5, FUNCOP_1:def_8; ::_thesis: verum
end;
suppose i1 <> i2 ; ::_thesis: A . z is Function
hence  A . z is Function by A5, FUNCOP_1:def_8; ::_thesis: verum
end;
end;
end;
then reconsider A = A as ManySortedFunction of the InternalRel of P by FUNCOP_1:def_6;
now__::_thesis:_for_i,_j,_k_being_Element_of_P_st_i_>=_j_&_j_>=_k_holds_
ex_f1_being_ManySortedFunction_of_(OAF_._i),(OAF_._j)_ex_f2_being_ManySortedFunction_of_(OAF_._j),(OAF_._k)_st_
(_f1_=_A_._(j,i)_&_f2_=_A_._(k,j)_&_A_._(k,i)_=_f2_**_f1_&_f1_is_homomorphism_OAF_._i,OAF_._j_)
let i, j, k be Element of P; ::_thesis: ( i >= j & j >= k implies ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = A . (j,i) & f2 = A . (k,j) & A . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) )
assume that
A6: i >= j and
A7: j >= k ; ::_thesis: ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = A . (j,i) & f2 = A . (k,j) & A . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j )
consider kl being set  such that
A8: kl = [j,i] ;
 kl in the InternalRel of P by A6, A8, ORDERS_2:def_5;
then consider i1, j1 being Element of P such that
A9: [j1,i1] = kl and
A10: A . kl = IFEQ (j1,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,j1)) ** (id the Sorts of (OAF . i1)))) by A4;
A11: ( i1 = i & j1 = j ) by A8, A9, XTUPLE_0:1;
 A . (j,i) is ManySortedFunction of (OAF . i),(OAF . j)
proof
percases ( i = j or i <> j ) ;
suppose i = j ; ::_thesis: A . (j,i) is ManySortedFunction of (OAF . i),(OAF . j)
hence  A . (j,i) is ManySortedFunction of (OAF . i),(OAF . j) by A9, A10, A11, FUNCOP_1:def_8; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: A . (j,i) is ManySortedFunction of (OAF . i),(OAF . j)
hence  A . (j,i) is ManySortedFunction of (OAF . i),(OAF . j) by A9, A10, A11, FUNCOP_1:def_8; ::_thesis: verum
end;
end;
end;
then reconsider f1 = A . (j,i) as ManySortedFunction of (OAF . i),(OAF . j) ;
consider lm being set  such that
A12: lm = [k,j] ;
 lm in the InternalRel of P by A7, A12, ORDERS_2:def_5;
then consider i2, j2 being Element of P such that
A13: [j2,i2] = lm and
A14: A . lm = IFEQ (j2,i2,(id the Sorts of (OAF . i2)),((bind (B,i2,j2)) ** (id the Sorts of (OAF . i2)))) by A4;
A15: ( j2 = k & i2 = j ) by A12, A13, XTUPLE_0:1;
 A . (k,j) is ManySortedFunction of (OAF . j),(OAF . k)
proof
percases ( j = k or j <> k ) ;
suppose j = k ; ::_thesis: A . (k,j) is ManySortedFunction of (OAF . j),(OAF . k)
hence  A . (k,j) is ManySortedFunction of (OAF . j),(OAF . k) by A13, A14, A15, FUNCOP_1:def_8; ::_thesis: verum
end;
suppose j <> k ; ::_thesis: A . (k,j) is ManySortedFunction of (OAF . j),(OAF . k)
hence  A . (k,j) is ManySortedFunction of (OAF . j),(OAF . k) by A13, A14, A15, FUNCOP_1:def_8; ::_thesis: verum
end;
end;
end;
then reconsider f2 = A . (k,j) as ManySortedFunction of (OAF . j),(OAF . k) ;
A16: for i, j being Element of P st i >= j & i <> j holds
A . (j,i) = bind (B,i,j)
proof
let i, j be Element of P; ::_thesis: ( i >= j & i <> j implies A . (j,i) = bind (B,i,j) )
assume that
A17: i >= j and
A18: i <> j ; ::_thesis: A . (j,i) = bind (B,i,j)
consider lm being set  such that
A19: lm = [j,i] ;
 lm in the InternalRel of P by A17, A19, ORDERS_2:def_5;
then consider i2, j2 being Element of P such that
A20: [j2,i2] = lm and
A21: A . lm = IFEQ (j2,i2,(id the Sorts of (OAF . i2)),((bind (B,i2,j2)) ** (id the Sorts of (OAF . i2)))) by A4;
 ( i2 = i & j2 = j ) by A19, A20, XTUPLE_0:1;
then  A . (j,i) = (bind (B,i,j)) ** (id the Sorts of (OAF . i)) by A18, A20, A21, FUNCOP_1:def_8;
hence  A . (j,i) = bind (B,i,j) by MSUALG_3:3; ::_thesis: verum
end;
A22: A . (k,i) = f2 ** f1
proof
percases ( ( i = j & j = k ) or ( i = j & j <> k ) or ( i <> j & j = k ) or ( i <> j & j <> k ) ) ;
supposeA23: ( i = j & j = k ) ; ::_thesis: A . (k,i) = f2 ** f1
then  f2 = id the Sorts of (OAF . j) by A13, A14, A15, FUNCOP_1:def_8;
hence  A . (k,i) = f2 ** f1 by A23, MSUALG_3:3; ::_thesis: verum
end;
supposeA24: ( i = j & j <> k ) ; ::_thesis: A . (k,i) = f2 ** f1
then  f1 = id the Sorts of (OAF . i) by A9, A10, A11, FUNCOP_1:def_8;
hence  A . (k,i) = f2 ** f1 by A24, MSUALG_3:3; ::_thesis: verum
end;
supposeA25: ( i <> j & j = k ) ; ::_thesis: A . (k,i) = f2 ** f1
then  f2 = id the Sorts of (OAF . j) by A13, A14, A15, FUNCOP_1:def_8;
hence  A . (k,i) = f2 ** f1 by A25, MSUALG_3:4; ::_thesis: verum
end;
supposeA26: ( i <> j & j <> k ) ; ::_thesis: A . (k,i) = f2 ** f1
then  ( i > j & j > k ) by A6, A7, ORDERS_2:def_6;
then A27: i <> k by ORDERS_2:5;
 f2 = (bind (B,j,k)) ** (id the Sorts of (OAF . j)) by A13, A14, A15, A26, FUNCOP_1:def_8;
then A28: f2 = bind (B,j,k) by MSUALG_3:3;
 f1 = (bind (B,i,j)) ** (id the Sorts of (OAF . i)) by A9, A10, A11, A26, FUNCOP_1:def_8;
then  f1 = bind (B,i,j) by MSUALG_3:3;
then  f2 ** f1 = bind (B,i,k) by A6, A7, A28, Th1;
hence  A . (k,i) = f2 ** f1 by A6, A7, A16, A27, ORDERS_2:3; ::_thesis: verum
end;
end;
end;
A29: for i, j being Element of P st i = j holds
A . (j,i) = id the Sorts of (OAF . i)
proof
let i, j be Element of P; ::_thesis: ( i = j implies A . (j,i) = id the Sorts of (OAF . i) )
consider lm being set  such that
A30: lm = [j,i] ;
assume A31: i = j ; ::_thesis: A . (j,i) = id the Sorts of (OAF . i)
then  i >= j by ORDERS_2:1;
then  lm in the InternalRel of P by A30, ORDERS_2:def_5;
then consider i2, j2 being Element of P such that
A32: [j2,i2] = lm and
A33: A . lm = IFEQ (j2,i2,(id the Sorts of (OAF . i2)),((bind (B,i2,j2)) ** (id the Sorts of (OAF . i2)))) by A4;
 ( i2 = i & j2 = j ) by A30, A32, XTUPLE_0:1;
hence  A . (j,i) = id the Sorts of (OAF . i) by A31, A32, A33, FUNCOP_1:def_8; ::_thesis: verum
end;
 f1 is_homomorphism OAF . i,OAF . j
proof
percases ( i = j or i <> j ) ;
supposeA34: i = j ; ::_thesis: f1 is_homomorphism OAF . i,OAF . j
then  A . (i,j) = id the Sorts of (OAF . i) by A29;
hence  f1 is_homomorphism OAF . i,OAF . j by A34, MSUALG_3:9; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: f1 is_homomorphism OAF . i,OAF . j
then  A . (j,i) = bind (B,i,j) by A6, A16;
hence  f1 is_homomorphism OAF . i,OAF . j by A6, Th2; ::_thesis: verum
end;
end;
end;
hence  ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = A . (j,i) & f2 = A . (k,j) & A . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by A22; ::_thesis: verum
end;
then reconsider A = A as Binding of OAF by Def2;
take  A ; ::_thesis: for i, j being Element of P st i >= j holds
A . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i))))
let i, j be Element of P; ::_thesis: ( i >= j implies A . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) )
consider kl being set  such that
A35: kl = [j,i] ;
assume  i >= j ; ::_thesis: A . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i))))
then  kl in the InternalRel of P by A35, ORDERS_2:def_5;
then consider i1, j1 being Element of P such that
A36: [j1,i1] = kl and
A37: A . kl = IFEQ (j1,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,j1)) ** (id the Sorts of (OAF . i1)))) by A4;
 ( i1 = i & j1 = j ) by A35, A36, XTUPLE_0:1;
hence  A . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) by A36, A37; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Binding of OAF st ( for i, j being Element of P st i >= j holds
b1 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ) & ( for i, j being Element of P st i >= j holds
b2 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ) holds
b1 = b2
proof
let N1, N2 be Binding of OAF; ::_thesis: ( ( for i, j being Element of P st i >= j holds
N1 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ) & ( for i, j being Element of P st i >= j holds
N2 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ) implies N1 = N2 )
assume that
A38: for i, j being Element of P st i >= j holds
N1 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) and
A39: for i, j being Element of P st i >= j holds
N2 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ; ::_thesis: N1 = N2
now__::_thesis:_for_ij_being_set_st_ij_in_the_InternalRel_of_P_holds_
N1_._ij_=_N2_._ij
let ij be set ; ::_thesis: ( ij in the InternalRel of P implies N1 . ij = N2 . ij )
assume A40: ij in the InternalRel of P ; ::_thesis: N1 . ij = N2 . ij
then reconsider i2 = ij `1 , i1 = ij `2 as Element of P by MCART_1:10;
reconsider i1 = i1, i2 = i2 as Element of P ;
A41: N2 . ij = N2 . (i2,i1) by A40, MCART_1:21;
 ij = [(ij `1),(ij `2)] by A40, MCART_1:21;
then A42: i2 <= i1 by A40, ORDERS_2:def_5;
 N1 . ij = N1 . (i2,i1) by A40, MCART_1:21;
then  N1 . ij = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) by A38, A42;
hence  N1 . ij = N2 . ij by A39, A42, A41; ::_thesis: verum
end;
hence  N1 = N2 by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Normalized MSALIMIT:def_5_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B, b5 being Binding of OAF holds
( b5 = Normalized B iff for i, j being Element of P st i >= j holds
b5 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) );

theorem Th3: :: MSALIMIT:3
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j & i <> j holds
B . (j,i) = (Normalized B) . (j,i)
proof
let P be non empty Poset; ::_thesis: for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j & i <> j holds
B . (j,i) = (Normalized B) . (j,i)
let S be non empty non void ManySortedSign ; ::_thesis: for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j & i <> j holds
B . (j,i) = (Normalized B) . (j,i)
let OAF be OrderedAlgFam of P,S; ::_thesis: for B being Binding of OAF
for i, j being Element of P st i >= j & i <> j holds
B . (j,i) = (Normalized B) . (j,i)
let B be Binding of OAF; ::_thesis: for i, j being Element of P st i >= j & i <> j holds
B . (j,i) = (Normalized B) . (j,i)
let i, j be Element of P; ::_thesis: ( i >= j & i <> j implies B . (j,i) = (Normalized B) . (j,i) )
assume that
A1: i >= j and
A2: i <> j ; ::_thesis: B . (j,i) = (Normalized B) . (j,i)
 ( (Normalized B) . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) & IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) = (bind (B,i,j)) ** (id the Sorts of (OAF . i)) ) by A1, A2, Def5, FUNCOP_1:def_8;
then  (Normalized B) . (j,i) = bind (B,i,j) by MSUALG_3:3;
hence  B . (j,i) = (Normalized B) . (j,i) by A1, Def3; ::_thesis: verum
end;

registration
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
cluster Normalized B ->  normalized ;
coherence
 Normalized B is normalized
proof
let i be Element of P; :: according to MSALIMIT:def_4 ::_thesis: (Normalized B) . (i,i) = id the Sorts of (OAF . i)
 i >= i by ORDERS_2:1;
then  (Normalized B) . (i,i) = IFEQ (i,i,(id the Sorts of (OAF . i)),((bind (B,i,i)) ** (id the Sorts of (OAF . i)))) by Def5;
hence  (Normalized B) . (i,i) = id the Sorts of (OAF . i) by FUNCOP_1:def_8; ::_thesis: verum
end;
end;

registration
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
cluster Relation-like the InternalRel of P -defined Function-like total Function-yielding V42() normalized for Binding of OAF;
existence
 ex b1 being Binding of OAF st b1 is normalized
proof
set B = the Binding of OAF;
take  Normalized the Binding of OAF ; ::_thesis: Normalized the Binding of OAF is normalized
thus  Normalized the Binding of OAF is normalized ; ::_thesis: verum
end;
end;

theorem :: MSALIMIT:4
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for NB being normalized Binding of OAF
for i, j being Element of P st i >= j holds
(Normalized NB) . (j,i) = NB . (j,i)
proof
let P be non empty Poset; ::_thesis: for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for NB being normalized Binding of OAF
for i, j being Element of P st i >= j holds
(Normalized NB) . (j,i) = NB . (j,i)
let S be non empty non void ManySortedSign ; ::_thesis: for OAF being OrderedAlgFam of P,S
for NB being normalized Binding of OAF
for i, j being Element of P st i >= j holds
(Normalized NB) . (j,i) = NB . (j,i)
let OAF be OrderedAlgFam of P,S; ::_thesis: for NB being normalized Binding of OAF
for i, j being Element of P st i >= j holds
(Normalized NB) . (j,i) = NB . (j,i)
let NB be normalized Binding of OAF; ::_thesis: for i, j being Element of P st i >= j holds
(Normalized NB) . (j,i) = NB . (j,i)
let i, j be Element of P; ::_thesis: ( i >= j implies (Normalized NB) . (j,i) = NB . (j,i) )
assume A1: i >= j ; ::_thesis: (Normalized NB) . (j,i) = NB . (j,i)
percases ( i <> j or i = j ) ;
suppose i <> j ; ::_thesis: (Normalized NB) . (j,i) = NB . (j,i)
hence  (Normalized NB) . (j,i) = NB . (j,i) by A1, Th3; ::_thesis: verum
end;
supposeA2: i = j ; ::_thesis: (Normalized NB) . (j,i) = NB . (j,i)
 (Normalized NB) . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (NB,i,j)) ** (id the Sorts of (OAF . i)))) by A1, Def5;
then  (Normalized NB) . (j,i) = id the Sorts of (OAF . i) by A2, FUNCOP_1:def_8;
hence  (Normalized NB) . (j,i) = NB . (j,i) by A2, Def4; ::_thesis: verum
end;
end;
end;

definition
let P be non empty Poset;
let S be non empty non void ManySortedSign ;
let OAF be OrderedAlgFam of P,S;
let B be Binding of OAF;
func InvLim B ->  strict MSSubAlgebra of product OAF means :Def6: :: MSALIMIT:def 6
 for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of it . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j );
existence
 ex b1 being strict MSSubAlgebra of product OAF st
for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b1 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j )
proof
reconsider L = product OAF as non-empty MSAlgebra over S ;
deffunc H1( SortSymbol of S) ->  set =  {  f where f is Element of product (Carrier (OAF,$1)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . $1) . (f . i) = f . j  }  ;
consider C being ManySortedSet of the carrier of S such that
A1: for s being SortSymbol of S holds C . s = H1(s) from PBOOLE:sch_5();
 for i being set st i in the carrier of S holds
C . i c= (SORTS OAF) . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies C . i c= (SORTS OAF) . i )
assume  i in the carrier of S ; ::_thesis: C . i c= (SORTS OAF) . i
then reconsider s = i as SortSymbol of S ;
defpred S1[ Element of product (Carrier (OAF,s))] means  for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . ($1 . i) = $1 . j;
A2:  {  f where f is Element of product (Carrier (OAF,s)) : S1[f]  }  c= product (Carrier (OAF,s)) from FRAENKEL:sch_10();
 (SORTS OAF) . s = product (Carrier (OAF,s)) by PRALG_2:def_10;
hence  C . i c= (SORTS OAF) . i by A1, A2; ::_thesis: verum
end;
then  C c= SORTS OAF by PBOOLE:def_2;
then reconsider C = C as ManySortedSubset of SORTS OAF by PBOOLE:def_18;
reconsider C = C as MSSubset of (product OAF) by PRALG_2:12;
 for o being OperSymbol of S holds C is_closed_on o
proof
let o be OperSymbol of S; ::_thesis: C is_closed_on o
 rng ((Den (o,(product OAF))) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o
proof
reconsider MS = C as ManySortedSet of the carrier of S ;
reconsider K = (Den (o,(product OAF))) | (((C #) * the Arity of S) . o) as Function ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((Den (o,(product OAF))) | (((C #) * the Arity of S) . o)) or x in (C * the ResultSort of S) . o )
A3: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
assume A4: x in rng ((Den (o,(product OAF))) | (((C #) * the Arity of S) . o)) ; ::_thesis: x in (C * the ResultSort of S) . o
then consider y being set  such that
A5: y in dom K and
A6: x = K . y by FUNCT_1:def_3;
A7: dom K = (dom (Den (o,(product OAF)))) /\ (((C #) * the Arity of S) . o) by RELAT_1:61;
then  y in ((C #) * the Arity of S) . o by A5, XBOOLE_0:def_4;
then  y in (C #) . ( the Arity of S . o) by A3, FUNCT_1:13;
then  y in (C #) . (the_arity_of o) by MSUALG_1:def_1;
then A8: y in product (MS * (the_arity_of o)) by FINSEQ_2:def_5;
 x in Result (o,(product OAF)) by A4;
then  ( dom the ResultSort of S = the carrier' of S & x in ( the Sorts of (product OAF) * the ResultSort of S) . o ) by FUNCT_2:def_1, MSUALG_1:def_5;
then  x in the Sorts of (product OAF) . ( the ResultSort of S . o) by FUNCT_1:13;
then A9: x in (SORTS OAF) . ( the ResultSort of S . o) by PRALG_2:12;
then reconsider x1 = x as Function ;
 x in (SORTS OAF) . (the_result_sort_of o) by A9, MSUALG_1:def_2;
then A10: x is Element of product (Carrier (OAF,(the_result_sort_of o))) by PRALG_2:def_10;
A11: y in dom (Den (o,(product OAF))) by A5, A7, XBOOLE_0:def_4;
now__::_thesis:_for_s_being_SortSymbol_of_S_holds_x_in_C_._(the_result_sort_of_o)
let s be SortSymbol of S; ::_thesis: x in C . (the_result_sort_of o)
 for i, j being Element of P st i >= j holds
((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j
proof
reconsider OPE = (OPS OAF) . o as Function ;
A12: Den (o,(product OAF)) = the Charact of (product OAF) . o by MSUALG_1:def_6
.= (OPS OAF) . o by PRALG_2:12 ;
reconsider y = y as Function by A8;
let i, j be Element of P; ::_thesis: ( i >= j implies ((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j )
assume A13: i >= j ; ::_thesis: ((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j
reconsider Co = commute y as Function ;
set y1 = (commute y) . i;
A14: dom y = dom (MS * (the_arity_of o)) by A8, CARD_3:9;
A15: rng (the_arity_of o) c= dom MS
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng (the_arity_of o) or i in dom MS )
assume  i in rng (the_arity_of o) ; ::_thesis: i in dom MS
then  i in the carrier of S ;
hence  i in dom MS by PARTFUN1:def_2; ::_thesis: verum
end;
then A16: dom y = dom (the_arity_of o) by A14, RELAT_1:27;
then A17: dom y = Seg (len (the_arity_of o)) by FINSEQ_1:def_3;
 rng y c= Funcs ( the carrier of P,|.OAF.|)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng y or z in Funcs ( the carrier of P,|.OAF.|) )
assume  z in rng y ; ::_thesis: z in Funcs ( the carrier of P,|.OAF.|)
then consider n being set  such that
A18: n in dom y and
A19: z = y . n by FUNCT_1:def_3;
A20: n in dom (MS * (the_arity_of o)) by A8, A18, CARD_3:9;
then  n in dom (the_arity_of o) by A15, RELAT_1:27;
then  (the_arity_of o) . n = (the_arity_of o) /. n by PARTFUN1:def_6;
then reconsider Pa = (the_arity_of o) . n as SortSymbol of S ;
 z in (MS * (the_arity_of o)) . n by A8, A19, A20, CARD_3:9;
then  z in MS . ((the_arity_of o) . n) by A20, FUNCT_1:12;
then  z in  {  f where f is Element of product (Carrier (OAF,Pa)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pa) . (f . i) = f . j  }  by A1;
then A21: ex z9 being Element of product (Carrier (OAF,Pa)) st
( z9 = z & ( for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pa) . (z9 . i) = z9 . j ) ) ;
then reconsider z = z as Function ;
A22: dom z = dom (Carrier (OAF,Pa)) by A21, CARD_3:9
.= the carrier of P by PARTFUN1:def_2 ;
 rng z c= |.OAF.|
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in rng z or p in |.OAF.| )
assume  p in rng z ; ::_thesis: p in |.OAF.|
then consider r being set  such that
A23: r in dom z and
A24: z . r = p by FUNCT_1:def_3;
reconsider r9 = r as Element of P by A22, A23;
reconsider r9 = r9 as Element of P ;
 r9 in the carrier of P ;
then A25: ex U0 being MSAlgebra over S st
( U0 = OAF . r & (Carrier (OAF,Pa)) . r = the Sorts of U0 . Pa ) by PRALG_2:def_9;
 |.(OAF . r9).| in  {  |.(OAF . k).| where k is Element of P : verum  }  ;
then  |.(OAF . r9).| c= union  {  |.(OAF . k).| where k is Element of P : verum  }  by ZFMISC_1:74;
then A26: |.(OAF . r9).| c= |.OAF.| by PRALG_2:def_7;
 dom the Sorts of (OAF . r9) = the carrier of S by PARTFUN1:def_2;
then A27: the Sorts of (OAF . r9) . Pa in rng the Sorts of (OAF . r9) by FUNCT_1:def_3;
 dom z = dom (Carrier (OAF,Pa)) by A21, CARD_3:9;
then  p in (Carrier (OAF,Pa)) . r by A21, A23, A24, CARD_3:9;
then  p in union (rng the Sorts of (OAF . r9)) by A25, A27, TARSKI:def_4;
then  p in |.(OAF . r9).| by PRALG_2:def_6;
hence  p in |.OAF.| by A26; ::_thesis: verum
end;
hence  z in Funcs ( the carrier of P,|.OAF.|) by A22, FUNCT_2:def_2; ::_thesis: verum
end;
then A28: y in Funcs ((Seg (len (the_arity_of o))),(Funcs ( the carrier of P,|.OAF.|))) by A17, FUNCT_2:def_2;
percases ( the_arity_of o <> {} or the_arity_of o = {} ) ;
supposeA29: the_arity_of o <> {} ; ::_thesis: ((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j
A30: for t being set st t in dom (doms (OAF ?. o)) holds
Co . t in (doms (OAF ?. o)) . t
proof
let t be set ; ::_thesis: ( t in dom (doms (OAF ?. o)) implies Co . t in (doms (OAF ?. o)) . t )
assume  t in dom (doms (OAF ?. o)) ; ::_thesis: Co . t in (doms (OAF ?. o)) . t
then reconsider t = t as Element of P by PRALG_2:11;
reconsider yt = Co . t as Function ;
 dom (the_arity_of o) <> {} by A29;
then  Seg (len (the_arity_of o)) <> {} by FINSEQ_1:def_3;
then  Co in Funcs ( the carrier of P,(Funcs ((Seg (len (the_arity_of o))),|.OAF.|))) by A28, FUNCT_6:55;
then A31: ex ss being Function st
( ss = Co & dom ss = the carrier of P & rng ss c= Funcs ((Seg (len (the_arity_of o))),|.OAF.|) ) by FUNCT_2:def_2;
A32: Co . t in product ( the Sorts of (OAF . t) * (the_arity_of o))
proof
A33: dom ( the Sorts of (OAF . t) * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3
.= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ;
A34: dom y = Seg (len (the_arity_of o)) by A16, FINSEQ_1:def_3;
A35: for w being set st w in dom ( the Sorts of (OAF . t) * (the_arity_of o)) holds
yt . w in ( the Sorts of (OAF . t) * (the_arity_of o)) . w
proof
 dom (the_arity_of o) <> {} by A29;
then  Seg (len (the_arity_of o)) <> {} by FINSEQ_1:def_3;
then A36: y = commute (commute y) by A28, FUNCT_6:57;
let w be set ; ::_thesis: ( w in dom ( the Sorts of (OAF . t) * (the_arity_of o)) implies yt . w in ( the Sorts of (OAF . t) * (the_arity_of o)) . w )
reconsider Pi = (the_arity_of o) /. w as SortSymbol of S ;
A37: dom (Carrier (OAF,((the_arity_of o) /. w))) = the carrier of P by PARTFUN1:def_2;
assume A38: w in dom ( the Sorts of (OAF . t) * (the_arity_of o)) ; ::_thesis: yt . w in ( the Sorts of (OAF . t) * (the_arity_of o)) . w
then A39: w in dom (the_arity_of o) by A33, FINSEQ_1:def_3;
 y . w in (MS * (the_arity_of o)) . w by A8, A14, A33, A34, A38, CARD_3:9;
then A40: y . w in MS . ((the_arity_of o) . w) by A39, FUNCT_1:13;
reconsider y = y as Function-yielding Function by A36;
reconsider yw = y . w as Function ;
 y . w in MS . ((the_arity_of o) /. w) by A39, A40, PARTFUN1:def_6;
then  yw in  {  ff where ff is Element of product (Carrier (OAF,Pi)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pi) . (ff . i) = ff . j  }  by A1;
then  ex jg being Element of product (Carrier (OAF,Pi)) st
( jg = yw & ( for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pi) . (jg . i) = jg . j ) ) ;
then A41: yw . t in (Carrier (OAF,((the_arity_of o) /. w))) . t by A37, CARD_3:9;
 ex U0 being MSAlgebra over S st
( U0 = OAF . t & (Carrier (OAF,((the_arity_of o) /. w))) . t = the Sorts of U0 . ((the_arity_of o) /. w) ) by PRALG_2:def_9;
then (Carrier (OAF,((the_arity_of o) /. w))) . t = the Sorts of (OAF . t) . ((the_arity_of o) . w) by A39, PARTFUN1:def_6
.= ( the Sorts of (OAF . t) * (the_arity_of o)) . w by A39, FUNCT_1:13 ;
hence  yt . w in ( the Sorts of (OAF . t) * (the_arity_of o)) . w by A28, A33, A38, A41, FUNCT_6:56; ::_thesis: verum
end;
 Co . t in rng Co by A31, FUNCT_1:def_3;
then  ex ts being Function st
( ts = Co . t & dom ts = Seg (len (the_arity_of o)) & rng ts c= |.OAF.| ) by A31, FUNCT_2:def_2;
hence  Co . t in product ( the Sorts of (OAF . t) * (the_arity_of o)) by A33, A35, CARD_3:9; ::_thesis: verum
end;
 (doms (OAF ?. o)) . t = Args (o,(OAF . t)) by PRALG_2:11;
hence  Co . t in (doms (OAF ?. o)) . t by A32, PRALG_2:3; ::_thesis: verum
end;
A42: Co in product (doms (OAF ?. o))
proof
 dom (the_arity_of o) <> {} by A29;
then  Seg (len (the_arity_of o)) <> {} by FINSEQ_1:def_3;
then  Co in Funcs ( the carrier of P,(Funcs ((Seg (len (the_arity_of o))),|.OAF.|))) by A28, FUNCT_6:55;
then  ex Co9 being Function st
( Co9 = Co & dom Co9 = the carrier of P & rng Co9 c= Funcs ((Seg (len (the_arity_of o))),|.OAF.|) ) by FUNCT_2:def_2;
then  dom Co = dom (doms (OAF ?. o)) by PRALG_2:11;
hence  Co in product (doms (OAF ?. o)) by A30, CARD_3:9; ::_thesis: verum
end;
A43: OPE = IFEQ ((the_arity_of o),{},(commute (OAF ?. o)),(Commute (Frege (OAF ?. o)))) by PRALG_2:def_13;
then A44: y in dom (Commute (Frege (OAF ?. o))) by A11, A12, A29, FUNCOP_1:def_8;
reconsider y1 = (commute y) . i as Function ;
A45: dom (OAF ?. o) = the carrier of P by PARTFUN1:def_2;
A46: x1 = OPE . y by A5, A6, A12, FUNCT_1:47
.= (Commute (Frege (OAF ?. o))) . y by A29, A43, FUNCOP_1:def_8
.= (Frege (OAF ?. o)) . (commute y) by A44, PRALG_2:def_1
.= (OAF ?. o) .. (commute y) by A42, PRALG_2:def_2 ;
then A47: x1 . i = ((OAF ?. o) . i) . ((commute y) . i) by A45, PRALG_1:def_17
.= (Den (o,(OAF . i))) . y1 by PRALG_2:7 ;
 dom (the_arity_of o) <> {} by A29;
then  Seg (len (the_arity_of o)) <> {} by FINSEQ_1:def_3;
then  Co in Funcs ( the carrier of P,(Funcs ((Seg (len (the_arity_of o))),|.OAF.|))) by A28, FUNCT_6:55;
then A48: ex ss being Function st
( ss = Co & dom ss = the carrier of P & rng ss c= Funcs ((Seg (len (the_arity_of o))),|.OAF.|) ) by FUNCT_2:def_2;
 y1 in product ( the Sorts of (OAF . i) * (the_arity_of o))
proof
A49: dom ( the Sorts of (OAF . i) * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3
.= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ;
A50: for w being set st w in dom ( the Sorts of (OAF . i) * (the_arity_of o)) holds
y1 . w in ( the Sorts of (OAF . i) * (the_arity_of o)) . w
proof
 dom (the_arity_of o) <> {} by A29;
then  Seg (len (the_arity_of o)) <> {} by FINSEQ_1:def_3;
then A51: y = commute (commute y) by A28, FUNCT_6:57;
let w be set ; ::_thesis: ( w in dom ( the Sorts of (OAF . i) * (the_arity_of o)) implies y1 . w in ( the Sorts of (OAF . i) * (the_arity_of o)) . w )
reconsider Pi = (the_arity_of o) /. w as SortSymbol of S ;
A52: dom (Carrier (OAF,((the_arity_of o) /. w))) = the carrier of P by PARTFUN1:def_2;
assume A53: w in dom ( the Sorts of (OAF . i) * (the_arity_of o)) ; ::_thesis: y1 . w in ( the Sorts of (OAF . i) * (the_arity_of o)) . w
then A54: w in dom (the_arity_of o) by A49, FINSEQ_1:def_3;
 w in dom y by A16, A49, A53, FINSEQ_1:def_3;
then  y . w in (MS * (the_arity_of o)) . w by A8, A14, CARD_3:9;
then A55: y . w in MS . ((the_arity_of o) . w) by A54, FUNCT_1:13;
reconsider y = y as Function-yielding Function by A51;
reconsider yw = y . w as Function ;
 y . w in MS . ((the_arity_of o) /. w) by A54, A55, PARTFUN1:def_6;
then  yw in  {  ff where ff is Element of product (Carrier (OAF,Pi)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pi) . (ff . i) = ff . j  }  by A1;
then  ex jg being Element of product (Carrier (OAF,Pi)) st
( jg = yw & ( for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pi) . (jg . i) = jg . j ) ) ;
then A56: yw . i in (Carrier (OAF,((the_arity_of o) /. w))) . i by A52, CARD_3:9;
 ex U0 being MSAlgebra over S st
( U0 = OAF . i & (Carrier (OAF,((the_arity_of o) /. w))) . i = the Sorts of U0 . ((the_arity_of o) /. w) ) by PRALG_2:def_9;
then (Carrier (OAF,((the_arity_of o) /. w))) . i = the Sorts of (OAF . i) . ((the_arity_of o) . w) by A54, PARTFUN1:def_6
.= ( the Sorts of (OAF . i) * (the_arity_of o)) . w by A54, FUNCT_1:13 ;
hence  y1 . w in ( the Sorts of (OAF . i) * (the_arity_of o)) . w by A28, A49, A53, A56, FUNCT_6:56; ::_thesis: verum
end;
 Co . i in rng Co by A48, FUNCT_1:def_3;
then  ex ts being Function st
( ts = Co . i & dom ts = Seg (len (the_arity_of o)) & rng ts c= |.OAF.| ) by A48, FUNCT_2:def_2;
hence  y1 in product ( the Sorts of (OAF . i) * (the_arity_of o)) by A49, A50, CARD_3:9; ::_thesis: verum
end;
then reconsider y19 = y1 as Element of Args (o,(OAF . i)) by PRALG_2:3;
A57: bind (B,i,j) is_homomorphism OAF . i,OAF . j by A13, Th2;
 (bind (B,i,j)) # y19 = (commute y) . j
proof
A58: dom ((bind (B,i,j)) # y19) = dom (the_arity_of o) by MSUALG_3:6
.= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ;
then reconsider One = (bind (B,i,j)) # y19 as FinSequence by FINSEQ_1:def_2;
 dom (the_arity_of o) <> {} by A29;
then A59: Seg (len (the_arity_of o)) <> {} by FINSEQ_1:def_3;
then  y = commute (commute y) by A28, FUNCT_6:57;
then reconsider y = y as Function-yielding Function ;
reconsider y2 = (commute y) . j as Function ;
 Co in Funcs ( the carrier of P,(Funcs ((Seg (len (the_arity_of o))),|.OAF.|))) by A28, A59, FUNCT_6:55;
then A60: ex ss being Function st
( ss = Co & dom ss = the carrier of P & rng ss c= Funcs ((Seg (len (the_arity_of o))),|.OAF.|) ) by FUNCT_2:def_2;
then  Co . j in rng Co by FUNCT_1:def_3;
then A61: ex ts being Function st
( ts = Co . j & dom ts = Seg (len (the_arity_of o)) & rng ts c= |.OAF.| ) by A60, FUNCT_2:def_2;
then reconsider Two = y2 as FinSequence by FINSEQ_1:def_2;
A62: Co . i in rng Co by A60, FUNCT_1:def_3;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_y2_holds_
((bind_(B,i,j))_#_y19)_._n_=_y2_._n
let n be Nat; ::_thesis: ( n in dom y2 implies ((bind (B,i,j)) # y19) . n = y2 . n )
reconsider yn = y . n as Function ;
reconsider Pi = (the_arity_of o) /. n as SortSymbol of S ;
A63: ex ts9 being Function st
( ts9 = Co . i & dom ts9 = Seg (len (the_arity_of o)) & rng ts9 c= |.OAF.| ) by A60, A62, FUNCT_2:def_2;
assume A64: n in dom y2 ; ::_thesis: ((bind (B,i,j)) # y19) . n = y2 . n
then A65: y . n in (MS * (the_arity_of o)) . n by A8, A14, A17, A61, CARD_3:9;
A66: n in dom (the_arity_of o) by A61, A64, FINSEQ_1:def_3;
then  (the_arity_of o) /. n = (the_arity_of o) . n by PARTFUN1:def_6;
then  yn in MS . Pi by A66, A65, FUNCT_1:13;
then  yn in  {  f where f is Element of product (Carrier (OAF,Pi)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pi) . (f . i) = f . j  }  by A1;
then A67: ex yn9 being Element of product (Carrier (OAF,Pi)) st
( yn9 = yn & ( for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pi) . (yn9 . i) = yn9 . j ) ) ;
 y19 . n = yn . i by A28, A61, A64, FUNCT_6:56;
then ((bind (B,i,j)) # y19) . n = ((bind (B,i,j)) . ((the_arity_of o) /. n)) . (yn . i) by A61, A64, A63, MSUALG_3:def_6
.= yn . j by A13, A67 ;
hence  ((bind (B,i,j)) # y19) . n = y2 . n by A28, A61, A64, FUNCT_6:56; ::_thesis: verum
end;
then  for n being Nat st n in Seg (len (the_arity_of o)) holds
One . n = Two . n by A61;
hence  (bind (B,i,j)) # y19 = (commute y) . j by A61, A58, FINSEQ_1:13; ::_thesis: verum
end;
then (Den (o,(OAF . j))) . ((bind (B,i,j)) # y19) = ((OAF ?. o) . j) . ((commute y) . j) by PRALG_2:7
.= x1 . j by A45, A46, PRALG_1:def_17 ;
hence  ((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j by A57, A47, MSUALG_3:def_7; ::_thesis: verum
end;
supposeA68: the_arity_of o = {} ; ::_thesis: ((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j
reconsider co = (commute (OAF ?. o)) . y as Function ;
A69: MS * {} = {} ;
A70: co = (curry' (uncurry (OAF ?. o))) . y by FUNCT_6:def_10;
A71: dom (OAF ?. o) = the carrier of P by PARTFUN1:def_2;
A72: Den (o,(product OAF)) = the Charact of (product OAF) . o by MSUALG_1:def_6
.= (OPS OAF) . o by PRALG_2:12
.= IFEQ ((the_arity_of o),{},(commute (OAF ?. o)),(Commute (Frege (OAF ?. o)))) by PRALG_2:def_13
.= commute (OAF ?. o) by A68, FUNCOP_1:def_8 ;
A73: for d being Element of P holds x1 . d = (Den (o,(OAF . d))) . {}
proof
reconsider co9 = (curry' (uncurry (OAF ?. o))) . y as Function by A70;
let d be Element of P; ::_thesis: x1 . d = (Den (o,(OAF . d))) . {}
reconsider g = (OAF ?. o) . d as Function ;
A74: x1 = (commute (OAF ?. o)) . y by A5, A6, A72, FUNCT_1:47;
 g = Den (o,(OAF . d)) by PRALG_2:7;
then  dom g = Args (o,(OAF . d)) by FUNCT_2:def_1
.= {{}} by A68, PRALG_2:4 ;
then A75: y in dom g by A8, A68, CARD_3:10;
then A76: [d,y] in dom (uncurry (OAF ?. o)) by A71, FUNCT_5:38;
co . d = co9 . d by FUNCT_6:def_10
.= (uncurry (OAF ?. o)) . (d,y) by A76, FUNCT_5:22
.= g . y by A71, A75, FUNCT_5:38 ;
then x1 . d = (Den (o,(OAF . d))) . y by A74, PRALG_2:7
.= (Den (o,(OAF . d))) . {} by A8, A68, A69, CARD_3:10, TARSKI:def_1 ;
hence  x1 . d = (Den (o,(OAF . d))) . {} ; ::_thesis: verum
end;
then A77: x1 . i = (Den (o,(OAF . i))) . {} ;
 Args (o,(OAF . i)) = {{}} by A68, PRALG_2:4;
then reconsider E = {} as Element of Args (o,(OAF . i)) by TARSKI:def_1;
set F = bind (B,i,j);
A78: Args (o,(OAF . j)) = {{}} by A68, PRALG_2:4;
 bind (B,i,j) is_homomorphism OAF . i,OAF . j by A13, Th2;
then A79: ((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = (Den (o,(OAF . j))) . ((bind (B,i,j)) # E) by A77, MSUALG_3:def_7;
 x1 . j = (Den (o,(OAF . j))) . {} by A73;
hence  ((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j by A79, A78, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
then  x in  {  f where f is Element of product (Carrier (OAF,(the_result_sort_of o))) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . (the_result_sort_of o)) . (f . i) = f . j  }  by A10;
hence  x in C . (the_result_sort_of o) by A1; ::_thesis: verum
end;
then  x in C . (the_result_sort_of o) ;
then A80: x in C . ( the ResultSort of S . o) by MSUALG_1:def_2;
 dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
hence  x in (C * the ResultSort of S) . o by A80, FUNCT_1:13; ::_thesis: verum
end;
hence  C is_closed_on o by MSUALG_2:def_5; ::_thesis: verum
end;
then A81: C is opers_closed by MSUALG_2:def_6;
reconsider C = C as MSSubset of L ;
set MSA = L | C;
A82: L | C = MSAlgebra(# C,(Opers (L,C)) #) by A81, MSUALG_2:def_15;
now__::_thesis:_for_s_being_SortSymbol_of_S
for_f_being_Element_of_(SORTS_OAF)_._s_holds_
(_f_in_the_Sorts_of_(L_|_C)_._s_iff_for_i,_j_being_Element_of_P_st_i_>=_j_holds_
((bind_(B,i,j))_._s)_._(f_._i)_=_f_._j_)
let s be SortSymbol of S; ::_thesis: for f being Element of (SORTS OAF) . s holds
( f in the Sorts of (L | C) . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j )
let f be Element of (SORTS OAF) . s; ::_thesis: ( f in the Sorts of (L | C) . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j )
A83: f is Element of product (Carrier (OAF,s)) by PRALG_2:def_10;
thus  ( f in the Sorts of (L | C) . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ::_thesis: verum
proof
hereby  ::_thesis: ( ( for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) implies f in the Sorts of (L | C) . s )
assume  f in the Sorts of (L | C) . s ; ::_thesis: for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j
then  f in  {  g where g is Element of product (Carrier (OAF,s)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (g . i) = g . j  }  by A1, A82;
then  ex k being Element of product (Carrier (OAF,s)) st
( k = f & ( for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (k . i) = k . j ) ) ;
hence  for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ; ::_thesis: verum
end;
assume  for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ; ::_thesis: f in the Sorts of (L | C) . s
then  f in  {  h where h is Element of product (Carrier (OAF,s)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (h . i) = h . j  }  by A83;
hence  f in the Sorts of (L | C) . s by A1, A82; ::_thesis: verum
end;
end;
hence  ex b1 being strict MSSubAlgebra of product OAF st
for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b1 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict MSSubAlgebra of product OAF st ( for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b1 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ) & ( for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b2 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ) holds
b1 = b2
proof
let A1, A2 be strict MSSubAlgebra of product OAF; ::_thesis: ( ( for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of A1 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ) & ( for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of A2 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ) implies A1 = A2 )
assume that
A84: for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of A1 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) and
A85: for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of A2 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ; ::_thesis: A1 = A2
 for s being set st s in the carrier of S holds
the Sorts of A1 . s = the Sorts of A2 . s
proof
let a be set ; ::_thesis: ( a in the carrier of S implies the Sorts of A1 . a = the Sorts of A2 . a )
assume  a in the carrier of S ; ::_thesis: the Sorts of A1 . a = the Sorts of A2 . a
then reconsider s = a as SortSymbol of S ;
thus  the Sorts of A1 . a c= the Sorts of A2 . a :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of A2 . a c= the Sorts of A1 . a
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the Sorts of A1 . a or e in the Sorts of A2 . a )
assume A86: e in the Sorts of A1 . a ; ::_thesis: e in the Sorts of A2 . a
 the Sorts of A1 is MSSubset of (product OAF) by MSUALG_2:def_9;
then  the Sorts of A1 c= the Sorts of (product OAF) by PBOOLE:def_18;
then  the Sorts of A1 c= SORTS OAF by PRALG_2:12;
then  the Sorts of A1 . s c= (SORTS OAF) . s by PBOOLE:def_2;
then reconsider f = e as Element of (SORTS OAF) . s by A86;
 for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j by A84, A86;
hence  e in the Sorts of A2 . a by A85; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the Sorts of A2 . a or e in the Sorts of A1 . a )
assume A87: e in the Sorts of A2 . a ; ::_thesis: e in the Sorts of A1 . a
 the Sorts of A2 is MSSubset of (product OAF) by MSUALG_2:def_9;
then  the Sorts of A2 c= the Sorts of (product OAF) by PBOOLE:def_18;
then  the Sorts of A2 c= SORTS OAF by PRALG_2:12;
then  the Sorts of A2 . s c= (SORTS OAF) . s by PBOOLE:def_2;
then reconsider f = e as Element of (SORTS OAF) . s by A87;
 for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j by A85, A87;
hence  e in the Sorts of A1 . a by A84; ::_thesis: verum
end;
hence  A1 = A2 by MSUALG_2:9, PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines InvLim MSALIMIT:def_6_:_
 for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for b5 being strict MSSubAlgebra of product OAF holds
( b5 = InvLim B iff for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b5 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) );

theorem :: MSALIMIT:5
for DP being non empty discrete Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of DP,S
for B being normalized Binding of OAF holds InvLim B = product OAF
proof
let DP be non empty discrete Poset; ::_thesis: for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of DP,S
for B being normalized Binding of OAF holds InvLim B = product OAF
let S be non empty non void ManySortedSign ; ::_thesis: for OAF being OrderedAlgFam of DP,S
for B being normalized Binding of OAF holds InvLim B = product OAF
let OAF be OrderedAlgFam of DP,S; ::_thesis: for B being normalized Binding of OAF holds InvLim B = product OAF
let B be normalized Binding of OAF; ::_thesis: InvLim B = product OAF
A1: for s being set st s in the carrier of S holds
the Sorts of (InvLim B) . s = the Sorts of (product OAF) . s
proof
let a be set ; ::_thesis: ( a in the carrier of S implies the Sorts of (InvLim B) . a = the Sorts of (product OAF) . a )
assume  a in the carrier of S ; ::_thesis: the Sorts of (InvLim B) . a = the Sorts of (product OAF) . a
then reconsider s = a as SortSymbol of S ;
thus  the Sorts of (InvLim B) . a c= the Sorts of (product OAF) . a :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of (product OAF) . a c= the Sorts of (InvLim B) . a
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the Sorts of (InvLim B) . a or e in the Sorts of (product OAF) . a )
 the Sorts of (InvLim B) is MSSubset of (product OAF) by MSUALG_2:def_9;
then  the Sorts of (InvLim B) c= the Sorts of (product OAF) by PBOOLE:def_18;
then A2: the Sorts of (InvLim B) . s c= the Sorts of (product OAF) . s by PBOOLE:def_2;
assume  e in the Sorts of (InvLim B) . a ; ::_thesis: e in the Sorts of (product OAF) . a
hence  e in the Sorts of (product OAF) . a by A2; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the Sorts of (product OAF) . a or e in the Sorts of (InvLim B) . a )
assume  e in the Sorts of (product OAF) . a ; ::_thesis: e in the Sorts of (InvLim B) . a
then reconsider f = e as Element of (SORTS OAF) . s by PRALG_2:12;
 for i, j being Element of DP st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j
proof
let i, j be Element of DP; ::_thesis: ( i >= j implies ((bind (B,i,j)) . s) . (f . i) = f . j )
assume  i >= j ; ::_thesis: ((bind (B,i,j)) . s) . (f . i) = f . j
then A3: i = j by ORDERS_3:1;
 f in (SORTS OAF) . s ;
then  ( dom (Carrier (OAF,s)) = the carrier of DP & f in product (Carrier (OAF,s)) ) by PARTFUN1:def_2, PRALG_2:def_10;
then A4: f . i in (Carrier (OAF,s)) . i by CARD_3:9;
bind (B,i,i) = B . (i,i) by Def3, ORDERS_2:1
.= id the Sorts of (OAF . i) by Def4 ;
then A5: (bind (B,i,i)) . s = id ( the Sorts of (OAF . i) . s) by MSUALG_3:def_1;
 ex U0 being MSAlgebra over S st
( U0 = OAF . i & (Carrier (OAF,s)) . i = the Sorts of U0 . s ) by PRALG_2:def_9;
hence  ((bind (B,i,j)) . s) . (f . i) = f . j by A3, A5, A4, FUNCT_1:18; ::_thesis: verum
end;
hence  e in the Sorts of (InvLim B) . a by Def6; ::_thesis: verum
end;
 product OAF is MSSubAlgebra of product OAF by MSUALG_2:5;
hence  InvLim B = product OAF by A1, MSUALG_2:9, PBOOLE:3; ::_thesis: verum
end;

begin


definition
let X be set ;
attrX is MSS-membered  means :Def7: :: MSALIMIT:def 7
 for x being set st x in X holds
x is non empty non void strict ManySortedSign ;
end;

:: deftheorem Def7 defines MSS-membered MSALIMIT:def_7_:_
 for X being set holds
( X is MSS-membered iff for x being set st x in X holds
x is non empty non void strict ManySortedSign );

registration
cluster non empty MSS-membered for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is MSS-membered )
proof
set S = the non empty non void strict ManySortedSign ;
set A = { the non empty non void strict ManySortedSign };
 for x being set st x in { the non empty non void strict ManySortedSign } holds
x is non empty non void strict ManySortedSign by TARSKI:def_1;
then  { the non empty non void strict ManySortedSign } is MSS-membered by Def7;
hence  ex b1 being set st
( not b1 is empty & b1 is MSS-membered ) ; ::_thesis: verum
end;
end;

definition
func TrivialMSSign  ->  strict ManySortedSign  means :Def8: :: MSALIMIT:def 8
( it is empty & it is void );
existence
 ex b1 being strict ManySortedSign st
( b1 is empty & b1 is void )
proof
 ( dom ({} --> {}) = {} & rng ({} --> {}) = {} ) ;
then reconsider g = {} --> {} as Function of {},{} by RELSET_1:4;
 {} in {} * by FINSEQ_1:49;
then reconsider f = {} --> {} as Function of {},({} *) by FUNCOP_1:46;
take  ManySortedSign(# {},{},f,g #) ; ::_thesis: ( ManySortedSign(# {},{},f,g #) is empty & ManySortedSign(# {},{},f,g #) is void )
thus  ( ManySortedSign(# {},{},f,g #) is empty & ManySortedSign(# {},{},f,g #) is void ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict ManySortedSign st b1 is empty & b1 is void & b2 is empty & b2 is void holds
b1 = b2
proof
let C1, C2 be strict ManySortedSign ; ::_thesis: ( C1 is empty & C1 is void & C2 is empty & C2 is void implies C1 = C2 )
assume that
A1: ( C1 is empty & C1 is void ) and
A2: ( C2 is empty & C2 is void ) ; ::_thesis: C1 = C2
 C1 = C2
proof
A3: ( the carrier of C1 = {} & the carrier' of C1 = {} ) by A1;
then reconsider RS = the ResultSort of C1, RT = the ResultSort of C2 as Function of {},{} by A2;
A4: ( the carrier of C2 = {} & the carrier' of C2 = {} ) by A2;
A5: RT in {(id {})} by ALTCAT_1:2, FUNCT_2:9;
 RS in {(id {})} by ALTCAT_1:2, FUNCT_2:9;
then  the ResultSort of C1 = id {}
.= the ResultSort of C2 by A5 ;
hence  C1 = C2 by A3, A4; ::_thesis: verum
end;
hence  C1 = C2 ; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines TrivialMSSign MSALIMIT:def_8_:_
 for b1 being strict ManySortedSign holds
( b1 = TrivialMSSign iff ( b1 is empty & b1 is void ) );

registration
cluster TrivialMSSign  ->  empty void strict ;
coherence
 ( TrivialMSSign is empty & TrivialMSSign is void ) by Def8;
end;

registration
cluster empty void strict for ManySortedSign ;
existence
 ex b1 being ManySortedSign st
( b1 is strict & b1 is empty & b1 is void )
proof
take  TrivialMSSign ; ::_thesis: ( TrivialMSSign is strict & TrivialMSSign is empty & TrivialMSSign is void )
thus  ( TrivialMSSign is strict & TrivialMSSign is empty & TrivialMSSign is void ) ; ::_thesis: verum
end;
end;

Lm1:  for S being empty void ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S
proof
let S be empty void ManySortedSign ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
set f = id the carrier of S;
 ( {} * the ResultSort of S = the ResultSort of S * {} & ( for o being set
for p being Function st o in the carrier' of S & p = the Arity of S . o holds
(id the carrier of S) * p = the Arity of S . ((id the carrier of S) . o) ) ) ;
hence  id the carrier of S, id the carrier' of S form_morphism_between S,S by PUA2MSS1:def_12, RELAT_1:38; ::_thesis: verum
end;

Lm2:  for S being non empty void ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S
proof
let S be non empty void ManySortedSign ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
set f = id the carrier of S;
set g = id the carrier' of S;
A1: ( rng (id the carrier of S) c= the carrier of S & rng (id the carrier' of S) c= the carrier' of S ) ;
A2: ( (id the carrier of S) * the ResultSort of S = {} & the ResultSort of S * (id the carrier' of S) = {} ) ;
A3: for o being set
for p being Function st o in the carrier' of S & p = the Arity of S . o holds
(id the carrier of S) * p = the Arity of S . ((id the carrier' of S) . o) ;
 ( dom (id the carrier of S) = the carrier of S & dom (id the carrier' of S) = the carrier' of S ) ;
hence  id the carrier of S, id the carrier' of S form_morphism_between S,S by A1, A2, A3, PUA2MSS1:def_12; ::_thesis: verum
end;

theorem :: MSALIMIT:6
for S being void ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S
proof
let S be void ManySortedSign ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
percases ( S is empty or not S is empty ) ;
suppose S is empty ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
hence  id the carrier of S, id the carrier' of S form_morphism_between S,S by Lm1; ::_thesis: verum
end;
suppose not S is empty ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
hence  id the carrier of S, id the carrier' of S form_morphism_between S,S by Lm2; ::_thesis: verum
end;
end;
end;

definition
let A be non empty set ;
func MSS_set A ->  set  means :Def9: :: MSALIMIT:def 9
 for x being set holds
( x in it iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) )
proof
defpred S1[ set , set ] means  ex S being non empty non void strict ManySortedSign st
( S = $2 & $1 = [ the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S] );
A1: for x, y, z being set st S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[x,z] implies y = z )
assume  ( S1[x,y] & S1[x,z] ) ; ::_thesis: y = z
then consider S1, S2 being non empty non void strict ManySortedSign  such that
A2: S1 = y and
A3: x = [ the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1] and
A4: S2 = z and
A5: x = [ the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2] and
 ( S2 is empty implies S2 is void ) ;
A6: the Arity of S1 = the Arity of S2 by A3, A5, XTUPLE_0:5;
 ( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 ) by A3, A5, XTUPLE_0:5;
hence  y = z by A2, A3, A4, A5, A6, XTUPLE_0:5; ::_thesis: verum
end;
consider X being set  such that
A7: for x being set holds
( x in X iff ex y being set st
( y in [:(bool A),(bool A),(PFuncs (A,(A *))),(PFuncs (A,A)):] & S1[y,x] ) ) from TARSKI:sch_1(A1);
take  X ; ::_thesis: for x being set holds
( x in X iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) )
let x be set ; ::_thesis: ( x in X iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) )
thus  ( x in X iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ::_thesis: verum
proof
thus  ( x in X implies ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ::_thesis: ( ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) implies x in X )
proof
assume  x in X ; ::_thesis: ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A )
then consider y being set  such that
A8: y in [:(bool A),(bool A),(PFuncs (A,(A *))),(PFuncs (A,A)):] and
A9: S1[y,x] by A7;
consider S being non empty non void strict ManySortedSign  such that
A10: S = x and
 y = [ the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S] by A9;
take  S ; ::_thesis: ( x = S & the carrier of S c= A & the carrier' of S c= A )
 ( the carrier of S in bool A & the carrier' of S in bool A ) by A8, A9, A10, MCART_1:80;
hence  ( x = S & the carrier of S c= A & the carrier' of S c= A ) by A10; ::_thesis: verum
end;
given S being non empty non void strict ManySortedSign  such that A11: x = S and
A12: the carrier of S c= A and
A13: the carrier' of S c= A ; ::_thesis: x in X
 ( dom the ResultSort of S = the carrier' of S & rng the ResultSort of S c= A ) by A12, FUNCT_2:def_1, XBOOLE_1:1;
then A14: the ResultSort of S in PFuncs (A,A) by A13, PARTFUN1:def_3;
reconsider C = the carrier of S as Subset of A by A12;
consider y being set  such that
A15: y = [ the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S] ;
 C * c= A * by MSUHOM_1:2;
then A16: rng the Arity of S c= A * by XBOOLE_1:1;
 dom the Arity of S c= A by A13, FUNCT_2:def_1;
then  the Arity of S in PFuncs (A,(A *)) by A16, PARTFUN1:def_3;
then  y in [:(bool A),(bool A),(PFuncs (A,(A *))),(PFuncs (A,A)):] by A12, A13, A15, A14, MCART_1:80;
hence  x in X by A7, A11, A15; ::_thesis: verum
end;
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) & ( for x being set holds
( x in b2 iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) holds
b1 = b2
proof
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) & ( for x being set holds
( x in A2 iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) implies A1 = A2 )
assume that
A17: for x being set holds
( x in A1 iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) and
A18: for x being set holds
( x in A2 iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ; ::_thesis: A1 = A2
thus  A1 c= A2 :: according to XBOOLE_0:def_10 ::_thesis: A2 c= A1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 or x in A2 )
assume  x in A1 ; ::_thesis: x in A2
then  ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) by A17;
hence  x in A2 by A18; ::_thesis: verum
end;
thus  A2 c= A1 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A2 or x in A1 )
assume  x in A2 ; ::_thesis: x in A1
then  ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) by A18;
hence  x in A1 by A17; ::_thesis: verum
end;
end;
end;

:: deftheorem Def9 defines MSS_set MSALIMIT:def_9_:_
 for A being non empty set
for b2 being set holds
( b2 = MSS_set A iff for x being set holds
( x in b2 iff ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) ) );

registration
let A be non empty set ;
cluster MSS_set A ->  non empty MSS-membered ;
coherence
 ( not MSS_set A is empty & MSS_set A is MSS-membered )
proof
set X = MSS_set A;
set a = the Element of A;
 ( dom ({ the Element of A} --> the Element of A) = { the Element of A} & rng ({ the Element of A} --> the Element of A) c= { the Element of A} ) by FUNCOP_1:13;
then reconsider g = { the Element of A} --> the Element of A as Function of { the Element of A},{ the Element of A} by FUNCT_2:2;
 the Element of A in { the Element of A} by TARSKI:def_1;
then  <* the Element of A*> in { the Element of A} * by FUNCT_7:18;
then reconsider f = { the Element of A} --> <* the Element of A*> as Function of { the Element of A},({ the Element of A} *) by FUNCOP_1:46;
A1: { the Element of A} c= A by ZFMISC_1:31;
 ManySortedSign(# { the Element of A},{ the Element of A},f,g #) in MSS_set A
proof
set SI = ManySortedSign(# { the Element of A},{ the Element of A},f,g #);
 ( not ManySortedSign(# { the Element of A},{ the Element of A},f,g #) is void & not ManySortedSign(# { the Element of A},{ the Element of A},f,g #) is empty ) ;
hence  ManySortedSign(# { the Element of A},{ the Element of A},f,g #) in MSS_set A by A1, Def9; ::_thesis: verum
end;
hence  not MSS_set A is empty ; ::_thesis: MSS_set A is MSS-membered
thus  MSS_set A is MSS-membered ::_thesis: verum
proof
let x be set ; :: according to MSALIMIT:def_7 ::_thesis: ( x in MSS_set A implies x is non empty non void strict ManySortedSign )
assume  x in MSS_set A ; ::_thesis: x is non empty non void strict ManySortedSign
then  ex S being non empty non void strict ManySortedSign st
( x = S & the carrier of S c= A & the carrier' of S c= A ) by Def9;
hence  x is non empty non void strict ManySortedSign ; ::_thesis: verum
end;
end;
end;

definition
let A be non empty MSS-membered set ;
:: original: Element
redefine mode Element of A ->  non empty non void strict ManySortedSign ;
coherence
 for b1 being Element of A holds b1 is non empty non void strict ManySortedSign by Def7;
end;

definition
let S1, S2 be ManySortedSign ;
func MSS_morph (S1,S2) ->  set  means :: MSALIMIT:def 10
 for x being set holds
( x in it iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) )
proof
defpred S1[ set ] means  ex f, g being Function st
( $1 = [f,g] & f,g form_morphism_between S1,S2 );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in [:(PFuncs ( the carrier of S1, the carrier of S2)),(PFuncs ( the carrier' of S1, the carrier' of S2)):] & S1[x] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for x being set holds
( x in X iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) )
thus  for x being set holds
( x in X iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in X iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) )
thus  ( x in X implies ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) by A1; ::_thesis: ( ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) implies x in X )
given f, g being Function such that A2: x = [f,g] and
A3: f,g form_morphism_between S1,S2 ; ::_thesis: x in X
 ( dom g = the carrier' of S1 & rng g c= the carrier' of S2 ) by A3, PUA2MSS1:def_12;
then A4: g in PFuncs ( the carrier' of S1, the carrier' of S2) by PARTFUN1:def_3;
 ( dom f = the carrier of S1 & rng f c= the carrier of S2 ) by A3, PUA2MSS1:def_12;
then  f in PFuncs ( the carrier of S1, the carrier of S2) by PARTFUN1:def_3;
then  x in [:(PFuncs ( the carrier of S1, the carrier of S2)),(PFuncs ( the carrier' of S1, the carrier' of S2)):] by A2, A4, ZFMISC_1:87;
hence  x in X by A1, A2, A3; ::_thesis: verum
end;
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ) & ( for x being set holds
( x in b2 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ) holds
b1 = b2
proof
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ) & ( for x being set holds
( x in A2 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ) implies A1 = A2 )
assume that
A5: for x being set holds
( x in A1 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) and
A6: for x being set holds
( x in A2 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ; ::_thesis: A1 = A2
A7: A2 c= A1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A2 or x in A1 )
assume  x in A2 ; ::_thesis: x in A1
then  ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) by A6;
hence  x in A1 by A5; ::_thesis: verum
end;
 A1 c= A2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 or x in A2 )
assume  x in A1 ; ::_thesis: x in A2
then  ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) by A5;
hence  x in A2 by A6; ::_thesis: verum
end;
hence  A1 = A2 by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem  defines MSS_morph MSALIMIT:def_10_:_
 for S1, S2 being ManySortedSign
for b3 being set holds
( b3 = MSS_morph (S1,S2) iff for x being set holds
( x in b3 iff ex f, g being Function st
( x = [f,g] & f,g form_morphism_between S1,S2 ) ) );