:: 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 ) ) );