:: MSUALG_9 semantic presentation begin registration let I be set ; let M be ManySortedSet of I; cluster Relation-like I -defined Function-like total V32() for Element of Bool M; existence not for b1 being Element of Bool M holds b1 is V32() proof [[0]] I c= M by PBOOLE:43; then [[0]] I is ManySortedSubset of M by PBOOLE:def_18; then reconsider A = [[0]] I as Element of Bool M by CLOSURE2:def_1; take A ; ::_thesis: A is V32() thus A is V32() ; ::_thesis: verum end; end; registration let I be set ; let M be V2() ManySortedSet of I; cluster Relation-like V2() I -defined Function-like total V32() for ManySortedSubset of M; existence ex b1 being ManySortedSubset of M st ( b1 is V2() & b1 is V32() ) proof defpred S1[ set , set ] means ex a being Element of M . I st M = {a}; A1: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ex_j_being_set_st_S1[i,j] let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume i in I ; ::_thesis: ex j being set st S1[i,j] set a = the Element of M . i; take j = { the Element of M . i}; ::_thesis: S1[i,j] thus S1[i,j] ; ::_thesis: verum end; consider C being ManySortedSet of I such that A2: for i being set st i in I holds S1[i,C . i] from PBOOLE:sch_3(A1); C is ManySortedSubset of M proof let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or C . i c= M . i ) assume A3: i in I ; ::_thesis: C . i c= M . i then A4: not M . i is empty ; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in C . i or q in M . i ) consider a being Element of M . i such that A5: C . i = {a} by A2, A3; assume q in C . i ; ::_thesis: q in M . i then q = a by A5, TARSKI:def_1; hence q in M . i by A4; ::_thesis: verum end; then reconsider C = C as ManySortedSubset of M ; take C ; ::_thesis: ( C is V2() & C is V32() ) thus C is V2() ::_thesis: C is V32() proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not C . i is empty ) assume i in I ; ::_thesis: not C . i is empty then ex a being Element of M . i st C . i = {a} by A2; hence not C . i is empty ; ::_thesis: verum end; let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or C . i is finite ) assume i in I ; ::_thesis: C . i is finite then ex a being Element of M . i st C . i = {a} by A2; hence C . i is finite ; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let o be OperSymbol of S; cluster -> FinSequence-like for Element of Args (o,A); coherence for b1 being Element of Args (o,A) holds b1 is FinSequence-like proof let x be Element of Args (o,A); ::_thesis: x is FinSequence-like dom x = dom (the_arity_of o) by MSUALG_6:2; then consider n being Nat such that A1: dom x = Seg n by FINSEQ_1:def_2; take n ; :: according to FINSEQ_1:def_2 ::_thesis: dom x = Seg n thus dom x = Seg n by A1; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let I be set ; let s be SortSymbol of S; let F be MSAlgebra-Family of I,S; cluster -> Relation-like Function-like for Element of (SORTS F) . s; coherence for b1 being Element of (SORTS F) . s holds ( b1 is Function-like & b1 is Relation-like ) proof let x be Element of (SORTS F) . s; ::_thesis: ( x is Function-like & x is Relation-like ) x is Element of product (Carrier (F,s)) by PRALG_2:def_10; hence ( x is Function-like & x is Relation-like ) ; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let X be V2() ManySortedSet of the carrier of S; cluster FreeGen X -> V2() free ; coherence ( FreeGen X is free & FreeGen X is non-empty ) by MSAFREE:14, MSAFREE:16; end; registration let S be non empty non void ManySortedSign ; let X be V2() ManySortedSet of the carrier of S; cluster FreeMSA X -> free ; coherence FreeMSA X is free by MSAFREE:17; end; registration let S be non empty non void ManySortedSign ; let A, B be non-empty MSAlgebra over S; cluster[:A,B:] -> non-empty ; coherence [:A,B:] is non-empty proof [:A,B:] = MSAlgebra(# [| the Sorts of A, the Sorts of B|],[[: the Charact of A, the Charact of B:]] #) by PRALG_2:def_8; hence the Sorts of [:A,B:] is V2() ; :: according to MSUALG_1:def_3 ::_thesis: verum end; end; theorem :: MSUALG_9:1 for a, X, Y being set for f being Function st a in dom f & f . a in [:X,Y:] holds f . a = [((pr1 f) . a),((pr2 f) . a)] proof let a be set ; ::_thesis: for X, Y being set for f being Function st a in dom f & f . a in [:X,Y:] holds f . a = [((pr1 f) . a),((pr2 f) . a)] let X, Y be set ; ::_thesis: for f being Function st a in dom f & f . a in [:X,Y:] holds f . a = [((pr1 f) . a),((pr2 f) . a)] let f be Function; ::_thesis: ( a in dom f & f . a in [:X,Y:] implies f . a = [((pr1 f) . a),((pr2 f) . a)] ) assume that A1: a in dom f and A2: f . a in [:X,Y:] ; ::_thesis: f . a = [((pr1 f) . a),((pr2 f) . a)] ( (pr1 f) . a = (f . a) `1 & (pr2 f) . a = (f . a) `2 ) by A1, MCART_1:def_12, MCART_1:def_13; hence f . a = [((pr1 f) . a),((pr2 f) . a)] by A2, MCART_1:21; ::_thesis: verum end; theorem Th2: :: MSUALG_9:2 for X being non empty set for Y being set for f being Function of X,{Y} holds rng f = {Y} proof let X be non empty set ; ::_thesis: for Y being set for f being Function of X,{Y} holds rng f = {Y} let Y be set ; ::_thesis: for f being Function of X,{Y} holds rng f = {Y} let f be Function of X,{Y}; ::_thesis: rng f = {Y} thus rng f c= {Y} ; :: according to XBOOLE_0:def_10 ::_thesis: {Y} c= rng f let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {Y} or q in rng f ) consider x being set such that A1: x in X by XBOOLE_0:def_1; assume q in {Y} ; ::_thesis: q in rng f then A2: ( dom f = X & q = Y ) by FUNCT_2:def_1, TARSKI:def_1; f . x = Y by A1, FUNCT_2:50; hence q in rng f by A2, A1, FUNCT_1:def_3; ::_thesis: verum end; theorem Th3: :: MSUALG_9:3 for I being set holds Class (nabla I) c= {I} proof let I be set ; ::_thesis: Class (nabla I) c= {I} let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Class (nabla I) or q in {I} ) assume q in Class (nabla I) ; ::_thesis: q in {I} then consider x being set such that A1: x in I and A2: q = Class ((nabla I),x) by EQREL_1:def_3; Class ((nabla I),x) = I by A1, EQREL_1:26; hence q in {I} by A2, TARSKI:def_1; ::_thesis: verum end; theorem Th4: :: MSUALG_9:4 for I being non empty set holds Class (nabla I) = {I} proof let I be non empty set ; ::_thesis: Class (nabla I) = {I} consider a being set such that A1: a in I by XBOOLE_0:def_1; thus Class (nabla I) c= {I} by Th3; :: according to XBOOLE_0:def_10 ::_thesis: {I} c= Class (nabla I) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {I} or q in Class (nabla I) ) assume q in {I} ; ::_thesis: q in Class (nabla I) then A2: q = I by TARSKI:def_1; Class ((nabla I),a) = I by A1, EQREL_1:26; hence q in Class (nabla I) by A2, A1, EQREL_1:def_3; ::_thesis: verum end; theorem Th5: :: MSUALG_9:5 for I, a being set ex A being ManySortedSet of I st {A} = I --> {a} proof let I, a be set ; ::_thesis: ex A being ManySortedSet of I st {A} = I --> {a} reconsider A = I --> a as ManySortedSet of I ; take A ; ::_thesis: {A} = I --> {a} now__::_thesis:_for_i_being_set_st_i_in_I_holds_ {A}_._i_=_(I_-->_{a})_._i let i be set ; ::_thesis: ( i in I implies {A} . i = (I --> {a}) . i ) assume A1: i in I ; ::_thesis: {A} . i = (I --> {a}) . i hence {A} . i = {(A . i)} by PZFMISC1:def_1 .= {a} by A1, FUNCOP_1:7 .= (I --> {a}) . i by A1, FUNCOP_1:7 ; ::_thesis: verum end; hence {A} = I --> {a} by PBOOLE:3; ::_thesis: verum end; theorem :: MSUALG_9:6 for I being set for A being ManySortedSet of I ex B being V2() ManySortedSet of I st A c= B proof let I be set ; ::_thesis: for A being ManySortedSet of I ex B being V2() ManySortedSet of I st A c= B let A be ManySortedSet of I; ::_thesis: ex B being V2() ManySortedSet of I st A c= B deffunc H1( set ) -> set = {{}} \/ (A . \$1); consider f being ManySortedSet of I such that A1: for i being set st i in I holds f . i = H1(i) from PBOOLE:sch_4(); f is V2() proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not f . i is empty ) assume i in I ; ::_thesis: not f . i is empty then f . i = {{}} \/ (A . i) by A1; hence not f . i is empty ; ::_thesis: verum end; then reconsider f = f as V2() ManySortedSet of I ; take f ; ::_thesis: A c= f let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= f . i ) assume i in I ; ::_thesis: A . i c= f . i then f . i = (A . i) \/ {{}} by A1; hence A . i c= f . i by XBOOLE_1:7; ::_thesis: verum end; theorem :: MSUALG_9:7 for I being set for M being V2() ManySortedSet of I for B being V32() ManySortedSubset of M ex C being V2() V32() ManySortedSubset of M st B c= C proof let I be set ; ::_thesis: for M being V2() ManySortedSet of I for B being V32() ManySortedSubset of M ex C being V2() V32() ManySortedSubset of M st B c= C let M be V2() ManySortedSet of I; ::_thesis: for B being V32() ManySortedSubset of M ex C being V2() V32() ManySortedSubset of M st B c= C let B be V32() ManySortedSubset of M; ::_thesis: ex C being V2() V32() ManySortedSubset of M st B c= C defpred S1[ set , set ] means ex a being Element of M . \$1 st \$2 = {a} \/ (B . \$1); A1: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ex_j_being_set_st_S1[i,j] let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume i in I ; ::_thesis: ex j being set st S1[i,j] set a = the Element of M . i; take j = { the Element of M . i} \/ (B . i); ::_thesis: S1[i,j] thus S1[i,j] ; ::_thesis: verum end; consider C being ManySortedSet of I such that A2: for i being set st i in I holds S1[i,C . i] from PBOOLE:sch_3(A1); A3: C is ManySortedSubset of M proof let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or C . i c= M . i ) assume A4: i in I ; ::_thesis: C . i c= M . i then consider a being Element of M . i such that A5: C . i = {a} \/ (B . i) by A2; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in C . i or q in M . i ) assume q in C . i ; ::_thesis: q in M . i then A6: ( q in {a} or q in B . i ) by A5, XBOOLE_0:def_3; B c= M by PBOOLE:def_18; then B . i c= M . i by A4, PBOOLE:def_2; then A7: ( q = a or q in M . i ) by A6, TARSKI:def_1; not M . i is empty by A4; hence q in M . i by A7; ::_thesis: verum end; A8: C is V32() proof let i be set ; :: according to FINSET_1:def_5 ::_thesis: ( not i in I or C . i is finite ) assume A9: i in I ; ::_thesis: C . i is finite reconsider b = B . i as finite set ; consider a being Element of M . i such that A10: C . i = {a} \/ (B . i) by A2, A9; thus C . i is finite by A10; ::_thesis: verum end; C is V2() proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not C . i is empty ) assume i in I ; ::_thesis: not C . i is empty then ex a being Element of M . i st C . i = {a} \/ (B . i) by A2; hence not C . i is empty ; ::_thesis: verum end; then reconsider C = C as V2() V32() ManySortedSubset of M by A3, A8; take C ; ::_thesis: B c= C let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or B . i c= C . i ) assume i in I ; ::_thesis: B . i c= C . i then ex a being Element of M . i st C . i = {a} \/ (B . i) by A2; hence B . i c= C . i by XBOOLE_1:7; ::_thesis: verum end; theorem :: MSUALG_9:8 for I being set for A, B being ManySortedSet of I for F, G being ManySortedFunction of A,{B} holds F = G proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for F, G being ManySortedFunction of A,{B} holds F = G let A, B be ManySortedSet of I; ::_thesis: for F, G being ManySortedFunction of A,{B} holds F = G let F, G be ManySortedFunction of A,{B}; ::_thesis: F = G now__::_thesis:_for_i_being_set_st_i_in_I_holds_ F_._i_=_G_._i let i be set ; ::_thesis: ( i in I implies F . i = G . i ) assume A1: i in I ; ::_thesis: F . i = G . i then A2: {B} . i = {(B . i)} by PZFMISC1:def_1; ( F . i is Function of (A . i),({B} . i) & G . i is Function of (A . i),({B} . i) ) by A1, PBOOLE:def_15; hence F . i = G . i by A2, FUNCT_2:51; ::_thesis: verum end; hence F = G by PBOOLE:3; ::_thesis: verum end; theorem Th9: :: MSUALG_9:9 for I being set for A being V2() ManySortedSet of I for B being ManySortedSet of I for F being ManySortedFunction of A,{B} holds F is "onto" proof let I be set ; ::_thesis: for A being V2() ManySortedSet of I for B being ManySortedSet of I for F being ManySortedFunction of A,{B} holds F is "onto" let A be V2() ManySortedSet of I; ::_thesis: for B being ManySortedSet of I for F being ManySortedFunction of A,{B} holds F is "onto" let B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,{B} holds F is "onto" let F be ManySortedFunction of A,{B}; ::_thesis: F is "onto" let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng (F . i) = {B} . i ) assume A1: i in I ; ::_thesis: rng (F . i) = {B} . i then ( {B} . i = {(B . i)} & F . i is Function of (A . i),({B} . i) ) by PBOOLE:def_15, PZFMISC1:def_1; hence rng (F . i) = {B} . i by A1, Th2; ::_thesis: verum end; theorem Th10: :: MSUALG_9:10 for I being set for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of {A},B holds F is "1-1" proof let I be set ; ::_thesis: for A being ManySortedSet of I for B being V2() ManySortedSet of I for F being ManySortedFunction of {A},B holds F is "1-1" let A be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I for F being ManySortedFunction of {A},B holds F is "1-1" let B be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of {A},B holds F is "1-1" let F be ManySortedFunction of {A},B; ::_thesis: F is "1-1" now__::_thesis:_for_i_being_set_st_i_in_I_holds_ F_._i_is_one-to-one let i be set ; ::_thesis: ( i in I implies F . i is one-to-one ) assume i in I ; ::_thesis: F . i is one-to-one then ( {A} . i = {(A . i)} & F . i is Function of ({A} . i),(B . i) ) by PBOOLE:def_15, PZFMISC1:def_1; hence F . i is one-to-one by PARTFUN1:17; ::_thesis: verum end; hence F is "1-1" by MSUALG_3:1; ::_thesis: verum end; theorem :: MSUALG_9:11 for S being non empty non void ManySortedSign for X being V2() ManySortedSet of the carrier of S holds Reverse X is "1-1" proof let S be non empty non void ManySortedSign ; ::_thesis: for X being V2() ManySortedSet of the carrier of S holds Reverse X is "1-1" let X be V2() ManySortedSet of the carrier of S; ::_thesis: Reverse X is "1-1" for i being set st i in the carrier of S holds (Reverse X) . i is one-to-one proof set D = DTConMSA X; let i be set ; ::_thesis: ( i in the carrier of S implies (Reverse X) . i is one-to-one ) assume i in the carrier of S ; ::_thesis: (Reverse X) . i is one-to-one then reconsider s = i as SortSymbol of S ; set f = (Reverse X) . s; let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom ((Reverse X) . i) or not x2 in dom ((Reverse X) . i) or not ((Reverse X) . i) . x1 = ((Reverse X) . i) . x2 or x1 = x2 ) assume that A1: x1 in dom ((Reverse X) . i) and A2: x2 in dom ((Reverse X) . i) and A3: ((Reverse X) . i) . x1 = ((Reverse X) . i) . x2 ; ::_thesis: x1 = x2 A4: (Reverse X) . s = Reverse (s,X) by MSAFREE:def_18; then A5: dom ((Reverse X) . s) = FreeGen (s,X) by FUNCT_2:def_1; then consider a2 being set such that A6: a2 in X . s and A7: x2 = root-tree [a2,s] by A2, MSAFREE:def_15; A8: [a2,s] in Terminals (DTConMSA X) by A6, MSAFREE:7; then reconsider t2 = [a2,s] as Symbol of (DTConMSA X) ; t2 `2 = s by MCART_1:7; then root-tree t2 in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by A8; then root-tree t2 in FreeGen (s,X) by MSAFREE:13; then A9: ((Reverse X) . s) . x2 = [a2,s] `1 by A4, A7, MSAFREE:def_17 .= a2 ; consider a1 being set such that A10: a1 in X . s and A11: x1 = root-tree [a1,s] by A1, A5, MSAFREE:def_15; A12: [a1,s] in Terminals (DTConMSA X) by A10, MSAFREE:7; then reconsider t1 = [a1,s] as Symbol of (DTConMSA X) ; t1 `2 = s by MCART_1:7; then root-tree t1 in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by A12; then root-tree t1 in FreeGen (s,X) by MSAFREE:13; then ((Reverse X) . s) . x1 = [a1,s] `1 by A4, A11, MSAFREE:def_17 .= a1 ; hence x1 = x2 by A3, A11, A7, A9; ::_thesis: verum end; hence Reverse X is "1-1" by MSUALG_3:1; ::_thesis: verum end; theorem :: MSUALG_9:12 for I being set for A being V2() V32() ManySortedSet of I ex F being ManySortedFunction of I --> NAT,A st F is "onto" proof let I be set ; ::_thesis: for A being V2() V32() ManySortedSet of I ex F being ManySortedFunction of I --> NAT,A st F is "onto" let A be V2() V32() ManySortedSet of I; ::_thesis: ex F being ManySortedFunction of I --> NAT,A st F is "onto" defpred S1[ set , set ] means ex f being Function of NAT,(A . \$1) st ( \$2 = f & rng f = A . \$1 ); A1: for i being set st i in I holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume A2: i in I ; ::_thesis: ex j being set st S1[i,j] consider f being Function of NAT,(A . i) such that A3: rng f = A . i by A2, CARD_3:96; take f ; ::_thesis: S1[i,f] thus S1[i,f] by A3; ::_thesis: verum end; consider F being ManySortedSet of I such that A4: for i being set st i in I holds S1[i,F . i] from PBOOLE:sch_3(A1); F is ManySortedFunction of I --> NAT,A proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or F . i is Element of bool [:((I --> NAT) . i),(A . i):] ) assume i in I ; ::_thesis: F . i is Element of bool [:((I --> NAT) . i),(A . i):] then ( ex f being Function of NAT,(A . i) st ( F . i = f & rng f = A . i ) & (I --> NAT) . i = NAT ) by A4, FUNCOP_1:7; hence F . i is Element of bool [:((I --> NAT) . i),(A . i):] ; ::_thesis: verum end; then reconsider F = F as ManySortedFunction of I --> NAT,A ; take F ; ::_thesis: F is "onto" let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng (F . i) = A . i ) assume i in I ; ::_thesis: rng (F . i) = A . i then ex f being Function of NAT,(A . i) st ( F . i = f & rng f = A . i ) by A4; hence rng (F . i) = A . i ; ::_thesis: verum end; theorem :: MSUALG_9:13 for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for f, g being Element of product the Sorts of A st ( for i being set holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) holds f = g proof let S be non empty ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for f, g being Element of product the Sorts of A st ( for i being set holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) holds f = g let A be non-empty MSAlgebra over S; ::_thesis: for f, g being Element of product the Sorts of A st ( for i being set holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) holds f = g let f, g be Element of product the Sorts of A; ::_thesis: ( ( for i being set holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ) implies f = g ) assume A1: for i being set holds (proj ( the Sorts of A,i)) . f = (proj ( the Sorts of A,i)) . g ; ::_thesis: f = g set X = the Sorts of A; now__::_thesis:_(_dom_f_=_dom_g_&_(_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_g_._x_)_) thus dom f = dom the Sorts of A by CARD_3:9 .= dom g by CARD_3:9 ; ::_thesis: for x being set st x in dom f holds f . x = g . x let x be set ; ::_thesis: ( x in dom f implies f . x = g . x ) assume x in dom f ; ::_thesis: f . x = g . x A2: dom (proj ( the Sorts of A,x)) = product the Sorts of A by CARD_3:def_16; hence f . x = (proj ( the Sorts of A,x)) . f by CARD_3:def_16 .= (proj ( the Sorts of A,x)) . g by A1 .= g . x by A2, CARD_3:def_16 ; ::_thesis: verum end; hence f = g by FUNCT_1:2; ::_thesis: verum end; theorem :: MSUALG_9:14 for S being non empty non void ManySortedSign for I being non empty set for s being Element of S for A being MSAlgebra-Family of I,S for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds f = g proof let S be non empty non void ManySortedSign ; ::_thesis: for I being non empty set for s being Element of S for A being MSAlgebra-Family of I,S for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds f = g let I be non empty set ; ::_thesis: for s being Element of S for A being MSAlgebra-Family of I,S for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds f = g let s be Element of S; ::_thesis: for A being MSAlgebra-Family of I,S for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds f = g let A be MSAlgebra-Family of I,S; ::_thesis: for f, g being Element of product (Carrier (A,s)) st ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) holds f = g let f, g be Element of product (Carrier (A,s)); ::_thesis: ( ( for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ) implies f = g ) assume A1: for a being Element of I holds (proj ((Carrier (A,s)),a)) . f = (proj ((Carrier (A,s)),a)) . g ; ::_thesis: f = g now__::_thesis:_(_dom_f_=_dom_g_&_(_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_g_._x_)_) dom f = dom (Carrier (A,s)) by CARD_3:9; hence dom f = dom g by CARD_3:9; ::_thesis: for x being set st x in dom f holds f . x = g . x let x be set ; ::_thesis: ( x in dom f implies f . x = g . x ) assume A2: x in dom f ; ::_thesis: f . x = g . x A3: dom (proj ((Carrier (A,s)),x)) = product (Carrier (A,s)) by CARD_3:def_16; hence f . x = (proj ((Carrier (A,s)),x)) . f by CARD_3:def_16 .= (proj ((Carrier (A,s)),x)) . g by A1, A2 .= g . x by A3, CARD_3:def_16 ; ::_thesis: verum end; hence f = g by FUNCT_1:2; ::_thesis: verum end; theorem :: MSUALG_9:15 for S being non empty non void ManySortedSign for A, B being non-empty MSAlgebra over S for C being non-empty MSSubAlgebra of A for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds for h2 being ManySortedFunction of B,A st h1 = h2 holds h2 is_homomorphism B,A proof let S be non empty non void ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over S for C being non-empty MSSubAlgebra of A for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds for h2 being ManySortedFunction of B,A st h1 = h2 holds h2 is_homomorphism B,A let A, B be non-empty MSAlgebra over S; ::_thesis: for C being non-empty MSSubAlgebra of A for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds for h2 being ManySortedFunction of B,A st h1 = h2 holds h2 is_homomorphism B,A let C be non-empty MSSubAlgebra of A; ::_thesis: for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds for h2 being ManySortedFunction of B,A st h1 = h2 holds h2 is_homomorphism B,A let h1 be ManySortedFunction of B,C; ::_thesis: ( h1 is_homomorphism B,C implies for h2 being ManySortedFunction of B,A st h1 = h2 holds h2 is_homomorphism B,A ) assume A1: h1 is_homomorphism B,C ; ::_thesis: for h2 being ManySortedFunction of B,A st h1 = h2 holds h2 is_homomorphism B,A the Sorts of C is ManySortedSubset of the Sorts of A by MSUALG_2:def_9; then id the Sorts of C is ManySortedFunction of C,A by EXTENS_1:5; then consider G being ManySortedFunction of C,A such that A2: G = id the Sorts of C ; G is_monomorphism C,A by A2, MSUALG_3:22; then A3: G is_homomorphism C,A by MSUALG_3:def_9; A4: G ** h1 = h1 by A2, MSUALG_3:4; let h2 be ManySortedFunction of B,A; ::_thesis: ( h1 = h2 implies h2 is_homomorphism B,A ) assume h1 = h2 ; ::_thesis: h2 is_homomorphism B,A hence h2 is_homomorphism B,A by A1, A4, A3, MSUALG_3:10; ::_thesis: verum end; theorem :: MSUALG_9:16 for S being non empty non void ManySortedSign for A, B being non-empty MSAlgebra over S for F being ManySortedFunction of A,B st F is_monomorphism A,B holds A, Image F are_isomorphic proof let S be non empty non void ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over S for F being ManySortedFunction of A,B st F is_monomorphism A,B holds A, Image F are_isomorphic let A, B be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,B st F is_monomorphism A,B holds A, Image F are_isomorphic let F be ManySortedFunction of A,B; ::_thesis: ( F is_monomorphism A,B implies A, Image F are_isomorphic ) assume A1: F is_monomorphism A,B ; ::_thesis: A, Image F are_isomorphic then F is_homomorphism A,B by MSUALG_3:def_9; then consider G being ManySortedFunction of A,(Image F) such that A2: G = F and A3: G is_epimorphism A, Image F by MSUALG_3:21; take G ; :: according to MSUALG_3:def_11 ::_thesis: G is_isomorphism A, Image F thus G is_epimorphism A, Image F by A3; :: according to MSUALG_3:def_10 ::_thesis: G is_monomorphism A, Image F thus G is_homomorphism A, Image F by A3, MSUALG_3:def_8; :: according to MSUALG_3:def_9 ::_thesis: G is "1-1" thus G is "1-1" by A1, A2, MSUALG_3:def_9; ::_thesis: verum end; theorem Th17: :: MSUALG_9:17 for S being non empty non void ManySortedSign for A, B being non-empty MSAlgebra over S for F being ManySortedFunction of A,B st F is "onto" holds for o being OperSymbol of S for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x proof let S be non empty non void ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over S for F being ManySortedFunction of A,B st F is "onto" holds for o being OperSymbol of S for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x let A, B be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,B st F is "onto" holds for o being OperSymbol of S for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x let F be ManySortedFunction of A,B; ::_thesis: ( F is "onto" implies for o being OperSymbol of S for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x ) assume A1: F is "onto" ; ::_thesis: for o being OperSymbol of S for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,B) ex y being Element of Args (o,A) st F # y = x let t be Element of Args (o,B); ::_thesis: ex y being Element of Args (o,A) st F # y = t set D = len (the_arity_of o); defpred S1[ set , set ] means ex y1 being Element of the Sorts of A . ((the_arity_of o) /. \$1) st ( (F . ((the_arity_of o) /. \$1)) . y1 = t . \$1 & \$2 = y1 ); A2: for k being Element of NAT st k in Seg (len (the_arity_of o)) holds ex x being set st S1[k,x] proof let k be Element of NAT ; ::_thesis: ( k in Seg (len (the_arity_of o)) implies ex x being set st S1[k,x] ) assume k in Seg (len (the_arity_of o)) ; ::_thesis: ex x being set st S1[k,x] then A3: k in dom (the_arity_of o) by FINSEQ_1:def_3; set s = (the_arity_of o) /. k; A4: t . k in the Sorts of B . ((the_arity_of o) /. k) by A3, MSUALG_6:2; rng (F . ((the_arity_of o) /. k)) = the Sorts of B . ((the_arity_of o) /. k) by A1, MSUALG_3:def_3; then consider y1 being set such that A5: y1 in the Sorts of A . ((the_arity_of o) /. k) and A6: (F . ((the_arity_of o) /. k)) . y1 = t . k by A4, FUNCT_2:11; reconsider y2 = y1 as Element of the Sorts of A . ((the_arity_of o) /. k) by A5; take y1 ; ::_thesis: S1[k,y1] take y2 ; ::_thesis: ( (F . ((the_arity_of o) /. k)) . y2 = t . k & y1 = y2 ) thus ( (F . ((the_arity_of o) /. k)) . y2 = t . k & y1 = y2 ) by A6; ::_thesis: verum end; consider p being FinSequence such that A7: dom p = Seg (len (the_arity_of o)) and A8: for k being Element of NAT st k in Seg (len (the_arity_of o)) holds S1[k,p . k] from MSUALG_8:sch_1(A2); A9: len p = len (the_arity_of o) by A7, FINSEQ_1:def_3; for k being Nat st k in dom p holds p . k in the Sorts of A . ((the_arity_of o) /. k) proof let k be Nat; ::_thesis: ( k in dom p implies p . k in the Sorts of A . ((the_arity_of o) /. k) ) assume k in dom p ; ::_thesis: p . k in the Sorts of A . ((the_arity_of o) /. k) then ex y1 being Element of the Sorts of A . ((the_arity_of o) /. k) st ( (F . ((the_arity_of o) /. k)) . y1 = t . k & p . k = y1 ) by A7, A8; hence p . k in the Sorts of A . ((the_arity_of o) /. k) ; ::_thesis: verum end; then reconsider p = p as Element of Args (o,A) by A9, MSAFREE2:5; set fp = F # p; take p ; ::_thesis: F # p = t reconsider E = the Sorts of B * (the_arity_of o) as V2() ManySortedSet of dom (the_arity_of o) ; A10: Args (o,B) = product E by PRALG_2:3; A11: Seg (len (the_arity_of o)) = dom (the_arity_of o) by FINSEQ_1:def_3 .= dom ( the Sorts of B * (the_arity_of o)) by PRALG_2:3 .= dom t by A10, CARD_3:9 ; A12: for k being Nat st k in dom t holds (F # p) . k = t . k proof let k be Nat; ::_thesis: ( k in dom t implies (F # p) . k = t . k ) assume A13: k in dom t ; ::_thesis: (F # p) . k = t . k then ex y1 being Element of the Sorts of A . ((the_arity_of o) /. k) st ( (F . ((the_arity_of o) /. k)) . y1 = t . k & p . k = y1 ) by A11, A8; hence (F # p) . k = t . k by A11, A7, A13, MSUALG_3:def_6; ::_thesis: verum end; dom (F # p) = dom ( the Sorts of B * (the_arity_of o)) by A10, CARD_3:9 .= dom t by A10, CARD_3:9 ; hence F # p = t by A12, FINSEQ_1:13; ::_thesis: verum end; theorem Th18: :: MSUALG_9:18 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for o being OperSymbol of S for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for o being OperSymbol of S for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) let A be non-empty MSAlgebra over S; ::_thesis: for o being OperSymbol of S for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) let x be Element of Args (o,A); ::_thesis: (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) (Den (o,A)) . x is Element of the Sorts of A . ( the ResultSort of S . o) by FUNCT_2:15; hence (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) ; ::_thesis: verum end; theorem Th19: :: MSUALG_9:19 for S being non empty non void ManySortedSign for A, B, C being non-empty MSAlgebra over S for F1 being ManySortedFunction of A,B for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds for G being ManySortedFunction of B,C st G ** F1 = F2 holds G is_homomorphism B,C proof let S be non empty non void ManySortedSign ; ::_thesis: for A, B, C being non-empty MSAlgebra over S for F1 being ManySortedFunction of A,B for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds for G being ManySortedFunction of B,C st G ** F1 = F2 holds G is_homomorphism B,C let A, B, C be non-empty MSAlgebra over S; ::_thesis: for F1 being ManySortedFunction of A,B for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds for G being ManySortedFunction of B,C st G ** F1 = F2 holds G is_homomorphism B,C let F1 be ManySortedFunction of A,B; ::_thesis: for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds for G being ManySortedFunction of B,C st G ** F1 = F2 holds G is_homomorphism B,C let F2 be ManySortedFunction of A,C; ::_thesis: ( F1 is_epimorphism A,B & F2 is_homomorphism A,C implies for G being ManySortedFunction of B,C st G ** F1 = F2 holds G is_homomorphism B,C ) assume that A1: F1 is_epimorphism A,B and A2: F2 is_homomorphism A,C ; ::_thesis: for G being ManySortedFunction of B,C st G ** F1 = F2 holds G is_homomorphism B,C let G be ManySortedFunction of B,C; ::_thesis: ( G ** F1 = F2 implies G is_homomorphism B,C ) assume A3: G ** F1 = F2 ; ::_thesis: G is_homomorphism B,C let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,B) = {} or for b1 being Element of Args (o,B) holds (G . (the_result_sort_of o)) . ((Den (o,B)) . b1) = (Den (o,C)) . (G # b1) ) assume Args (o,B) <> {} ; ::_thesis: for b1 being Element of Args (o,B) holds (G . (the_result_sort_of o)) . ((Den (o,B)) . b1) = (Den (o,C)) . (G # b1) let x be Element of Args (o,B); ::_thesis: (G . (the_result_sort_of o)) . ((Den (o,B)) . x) = (Den (o,C)) . (G # x) F1 is "onto" by A1, MSUALG_3:def_8; then consider y being Element of Args (o,A) such that A4: F1 # y = x by Th17; set r = the_result_sort_of o; F1 is_homomorphism A,B by A1, MSUALG_3:def_8; then A5: (F1 . (the_result_sort_of o)) . ((Den (o,A)) . y) = (Den (o,B)) . x by A4, MSUALG_3:def_7; A6: (F2 . (the_result_sort_of o)) . ((Den (o,A)) . y) = ((G . (the_result_sort_of o)) * (F1 . (the_result_sort_of o))) . ((Den (o,A)) . y) by A3, MSUALG_3:2 .= (G . (the_result_sort_of o)) . ((Den (o,B)) . x) by A5, Th18, FUNCT_2:15 ; (F2 . (the_result_sort_of o)) . ((Den (o,A)) . y) = (Den (o,C)) . ((G ** F1) # y) by A2, A3, MSUALG_3:def_7 .= (Den (o,C)) . (G # x) by A4, MSUALG_3:8 ; hence (G . (the_result_sort_of o)) . ((Den (o,B)) . x) = (Den (o,C)) . (G # x) by A6; ::_thesis: verum end; definition let I be set ; let A be ManySortedSet of I; let B, C be V2() ManySortedSet of I; let F be ManySortedFunction of A,[|B,C|]; func Mpr1 F -> ManySortedFunction of A,B means :Def1: :: MSUALG_9:def 1 for i being set st i in I holds it . i = pr1 (F . i); existence ex b1 being ManySortedFunction of A,B st for i being set st i in I holds b1 . i = pr1 (F . i) proof deffunc H1( set ) -> set = pr1 (F . \$1); consider X being ManySortedSet of I such that A1: for i being set st i in I holds X . i = H1(i) from PBOOLE:sch_4(); X is ManySortedFunction of A,B proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or X . i is Element of bool [:(A . i),(B . i):] ) assume A2: i in I ; ::_thesis: X . i is Element of bool [:(A . i),(B . i):] then reconsider Bi = B . i as non empty set ; A3: X . i = pr1 (F . i) by A1, A2; then reconsider Xi = X . i as Function ; A4: F . i is Function of (A . i),([|B,C|] . i) by A2, PBOOLE:def_15; A5: rng Xi c= Bi proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng Xi or q in Bi ) assume q in rng Xi ; ::_thesis: q in Bi then consider x being set such that A6: x in dom Xi and A7: Xi . x = q by FUNCT_1:def_3; x in dom (F . i) by A3, A6, MCART_1:def_12; then A8: ( Xi . x = ((F . i) . x) `1 & (F . i) . x in rng (F . i) ) by A3, FUNCT_1:def_3, MCART_1:def_12; rng (F . i) c= [|B,C|] . i by A4, RELAT_1:def_19; then A9: rng (F . i) c= [:(B . i),(C . i):] by A2, PBOOLE:def_16; assume not q in Bi ; ::_thesis: contradiction hence contradiction by A7, A9, A8, MCART_1:10; ::_thesis: verum end; dom (F . i) = A . i by A2, A4, FUNCT_2:def_1; then dom Xi = A . i by A3, MCART_1:def_12; hence X . i is Element of bool [:(A . i),(B . i):] by A5, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; then reconsider X = X as ManySortedFunction of A,B ; take X ; ::_thesis: for i being set st i in I holds X . i = pr1 (F . i) thus for i being set st i in I holds X . i = pr1 (F . i) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of A,B st ( for i being set st i in I holds b1 . i = pr1 (F . i) ) & ( for i being set st i in I holds b2 . i = pr1 (F . i) ) holds b1 = b2 proof let M, N be ManySortedFunction of A,B; ::_thesis: ( ( for i being set st i in I holds M . i = pr1 (F . i) ) & ( for i being set st i in I holds N . i = pr1 (F . i) ) implies M = N ) assume that A10: for i being set st i in I holds M . i = pr1 (F . i) and A11: for i being set st i in I holds N . i = pr1 (F . i) ; ::_thesis: M = N now__::_thesis:_for_i_being_set_st_i_in_I_holds_ M_._i_=_N_._i let i be set ; ::_thesis: ( i in I implies M . i = N . i ) assume A12: i in I ; ::_thesis: M . i = N . i hence M . i = pr1 (F . i) by A10 .= N . i by A11, A12 ; ::_thesis: verum end; hence M = N by PBOOLE:3; ::_thesis: verum end; func Mpr2 F -> ManySortedFunction of A,C means :Def2: :: MSUALG_9:def 2 for i being set st i in I holds it . i = pr2 (F . i); existence ex b1 being ManySortedFunction of A,C st for i being set st i in I holds b1 . i = pr2 (F . i) proof deffunc H1( set ) -> set = pr2 (F . \$1); consider X being ManySortedSet of I such that A13: for i being set st i in I holds X . i = H1(i) from PBOOLE:sch_4(); X is ManySortedFunction of A,C proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or X . i is Element of bool [:(A . i),(C . i):] ) assume A14: i in I ; ::_thesis: X . i is Element of bool [:(A . i),(C . i):] then reconsider Ci = C . i as non empty set ; A15: X . i = pr2 (F . i) by A13, A14; then reconsider Xi = X . i as Function ; A16: F . i is Function of (A . i),([|B,C|] . i) by A14, PBOOLE:def_15; A17: rng Xi c= Ci proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng Xi or q in Ci ) assume q in rng Xi ; ::_thesis: q in Ci then consider x being set such that A18: x in dom Xi and A19: Xi . x = q by FUNCT_1:def_3; x in dom (F . i) by A15, A18, MCART_1:def_13; then A20: ( Xi . x = ((F . i) . x) `2 & (F . i) . x in rng (F . i) ) by A15, FUNCT_1:def_3, MCART_1:def_13; rng (F . i) c= [|B,C|] . i by A16, RELAT_1:def_19; then A21: rng (F . i) c= [:(B . i),(C . i):] by A14, PBOOLE:def_16; assume not q in Ci ; ::_thesis: contradiction hence contradiction by A19, A21, A20, MCART_1:10; ::_thesis: verum end; dom (F . i) = A . i by A14, A16, FUNCT_2:def_1; then dom Xi = A . i by A15, MCART_1:def_13; hence X . i is Element of bool [:(A . i),(C . i):] by A17, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; then reconsider X = X as ManySortedFunction of A,C ; take X ; ::_thesis: for i being set st i in I holds X . i = pr2 (F . i) thus for i being set st i in I holds X . i = pr2 (F . i) by A13; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of A,C st ( for i being set st i in I holds b1 . i = pr2 (F . i) ) & ( for i being set st i in I holds b2 . i = pr2 (F . i) ) holds b1 = b2 proof let M, N be ManySortedFunction of A,C; ::_thesis: ( ( for i being set st i in I holds M . i = pr2 (F . i) ) & ( for i being set st i in I holds N . i = pr2 (F . i) ) implies M = N ) assume that A22: for i being set st i in I holds M . i = pr2 (F . i) and A23: for i being set st i in I holds N . i = pr2 (F . i) ; ::_thesis: M = N now__::_thesis:_for_i_being_set_st_i_in_I_holds_ M_._i_=_N_._i let i be set ; ::_thesis: ( i in I implies M . i = N . i ) assume A24: i in I ; ::_thesis: M . i = N . i hence M . i = pr2 (F . i) by A22 .= N . i by A23, A24 ; ::_thesis: verum end; hence M = N by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def1 defines Mpr1 MSUALG_9:def_1_:_ for I being set for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,[|B,C|] for b6 being ManySortedFunction of A,B holds ( b6 = Mpr1 F iff for i being set st i in I holds b6 . i = pr1 (F . i) ); :: deftheorem Def2 defines Mpr2 MSUALG_9:def_2_:_ for I being set for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,[|B,C|] for b6 being ManySortedFunction of A,C holds ( b6 = Mpr2 F iff for i being set st i in I holds b6 . i = pr2 (F . i) ); theorem :: MSUALG_9:20 for I, a being set for A being ManySortedSet of I for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F proof let I, a be set ; ::_thesis: for A being ManySortedSet of I for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F let A be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F let F be ManySortedFunction of A,[|(I --> {a}),(I --> {a})|]; ::_thesis: Mpr1 F = Mpr2 F now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (Mpr1_F)_._i_=_(Mpr2_F)_._i let i be set ; ::_thesis: ( i in I implies (Mpr1 F) . i = (Mpr2 F) . i ) A1: dom (pr2 (F . i)) = dom (F . i) by MCART_1:def_13; assume A2: i in I ; ::_thesis: (Mpr1 F) . i = (Mpr2 F) . i A3: now__::_thesis:_for_y_being_set_st_y_in_dom_(F_._i)_holds_ (pr2_(F_._i))_._y_=_((F_._i)_._y)_`1 let y be set ; ::_thesis: ( y in dom (F . i) implies (pr2 (F . i)) . y = ((F . i) . y) `1 ) assume A4: y in dom (F . i) ; ::_thesis: (pr2 (F . i)) . y = ((F . i) . y) `1 A5: (F . i) . y in rng (F . i) by A4, FUNCT_1:def_3; F . i is Function of (A . i),([|(I --> {a}),(I --> {a})|] . i) by A2, PBOOLE:def_15; then rng (F . i) c= [|(I --> {a}),(I --> {a})|] . i by RELAT_1:def_19; then A6: rng (F . i) c= [:((I --> {a}) . i),((I --> {a}) . i):] by A2, PBOOLE:def_16; then ((F . i) . y) `1 in (I --> {a}) . i by A5, MCART_1:10; then A7: ((F . i) . y) `1 in {a} by A2, FUNCOP_1:7; ((F . i) . y) `2 in (I --> {a}) . i by A5, A6, MCART_1:10; then A8: ((F . i) . y) `2 in {a} by A2, FUNCOP_1:7; thus (pr2 (F . i)) . y = ((F . i) . y) `2 by A4, MCART_1:def_13 .= a by A8, TARSKI:def_1 .= ((F . i) . y) `1 by A7, TARSKI:def_1 ; ::_thesis: verum end; ( (Mpr1 F) . i = pr1 (F . i) & (Mpr2 F) . i = pr2 (F . i) ) by A2, Def1, Def2; hence (Mpr1 F) . i = (Mpr2 F) . i by A1, A3, MCART_1:def_12; ::_thesis: verum end; hence Mpr1 F = Mpr2 F by PBOOLE:3; ::_thesis: verum end; theorem :: MSUALG_9:21 for I being set for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds Mpr1 F is "onto" proof let I be set ; ::_thesis: for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds Mpr1 F is "onto" let A be ManySortedSet of I; ::_thesis: for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds Mpr1 F is "onto" let B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds Mpr1 F is "onto" let F be ManySortedFunction of A,[|B,C|]; ::_thesis: ( F is "onto" implies Mpr1 F is "onto" ) assume A1: F is "onto" ; ::_thesis: Mpr1 F is "onto" let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng ((Mpr1 F) . i) = B . i ) assume A2: i in I ; ::_thesis: rng ((Mpr1 F) . i) = B . i then reconsider m = (Mpr1 F) . i as Function of (A . i),(B . i) by PBOOLE:def_15; rng m = B . i proof thus rng m c= B . i ; :: according to XBOOLE_0:def_10 ::_thesis: B . i c= rng m let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B . i or a in rng m ) assume A3: a in B . i ; ::_thesis: a in rng m consider z being set such that A4: z in [|B,C|] . i by A2, XBOOLE_0:def_1; set p = [a,(z `2)]; z in [:(B . i),(C . i):] by A2, A4, PBOOLE:def_16; then A5: [a,(z `2)] `2 in C . i by MCART_1:10; [a,(z `2)] `1 in B . i by A3; then [a,(z `2)] in [:(B . i),(C . i):] by A5, MCART_1:11; then A6: [a,(z `2)] in [|B,C|] . i by A2, PBOOLE:def_16; A7: dom m = A . i by A2, FUNCT_2:def_1; A8: F . i is Function of (A . i),([|B,C|] . i) by A2, PBOOLE:def_15; then A9: dom (F . i) = A . i by A2, FUNCT_2:def_1; rng (F . i) = [|B,C|] . i by A1, A2, MSUALG_3:def_3; then consider b being set such that A10: b in A . i and A11: (F . i) . b = [a,(z `2)] by A8, A6, FUNCT_2:11; m . b = (pr1 (F . i)) . b by A2, Def1 .= [a,(z `2)] `1 by A10, A11, A9, MCART_1:def_12 .= a ; hence a in rng m by A10, A7, FUNCT_1:def_3; ::_thesis: verum end; hence rng ((Mpr1 F) . i) = B . i ; ::_thesis: verum end; theorem :: MSUALG_9:22 for I being set for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds Mpr2 F is "onto" proof let I be set ; ::_thesis: for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds Mpr2 F is "onto" let A be ManySortedSet of I; ::_thesis: for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds Mpr2 F is "onto" let B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds Mpr2 F is "onto" let F be ManySortedFunction of A,[|B,C|]; ::_thesis: ( F is "onto" implies Mpr2 F is "onto" ) assume A1: F is "onto" ; ::_thesis: Mpr2 F is "onto" let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or rng ((Mpr2 F) . i) = C . i ) assume A2: i in I ; ::_thesis: rng ((Mpr2 F) . i) = C . i then reconsider m = (Mpr2 F) . i as Function of (A . i),(C . i) by PBOOLE:def_15; rng m = C . i proof thus rng m c= C . i ; :: according to XBOOLE_0:def_10 ::_thesis: C . i c= rng m let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in C . i or a in rng m ) assume A3: a in C . i ; ::_thesis: a in rng m consider z being set such that A4: z in [|B,C|] . i by A2, XBOOLE_0:def_1; set p = [(z `1),a]; z in [:(B . i),(C . i):] by A2, A4, PBOOLE:def_16; then A5: [(z `1),a] `1 in B . i by MCART_1:10; [(z `1),a] `2 in C . i by A3; then [(z `1),a] in [:(B . i),(C . i):] by A5, MCART_1:11; then A6: [(z `1),a] in [|B,C|] . i by A2, PBOOLE:def_16; A7: dom m = A . i by A2, FUNCT_2:def_1; A8: F . i is Function of (A . i),([|B,C|] . i) by A2, PBOOLE:def_15; then A9: dom (F . i) = A . i by A2, FUNCT_2:def_1; rng (F . i) = [|B,C|] . i by A1, A2, MSUALG_3:def_3; then consider b being set such that A10: b in A . i and A11: (F . i) . b = [(z `1),a] by A8, A6, FUNCT_2:11; m . b = (pr2 (F . i)) . b by A2, Def2 .= [(z `1),a] `2 by A10, A11, A9, MCART_1:def_13 .= a ; hence a in rng m by A10, A7, FUNCT_1:def_3; ::_thesis: verum end; hence rng ((Mpr2 F) . i) = C . i ; ::_thesis: verum end; theorem :: MSUALG_9:23 for I being set for A, M being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,[|B,C|] st M in doms F holds for i being set st i in I holds (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] proof let I be set ; ::_thesis: for A, M being ManySortedSet of I for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,[|B,C|] st M in doms F holds for i being set st i in I holds (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] let A, M be ManySortedSet of I; ::_thesis: for B, C being V2() ManySortedSet of I for F being ManySortedFunction of A,[|B,C|] st M in doms F holds for i being set st i in I holds (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] let B, C be V2() ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,[|B,C|] st M in doms F holds for i being set st i in I holds (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] let F be ManySortedFunction of A,[|B,C|]; ::_thesis: ( M in doms F implies for i being set st i in I holds (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] ) assume A1: M in doms F ; ::_thesis: for i being set st i in I holds (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] let i be set ; ::_thesis: ( i in I implies (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] ) assume A2: i in I ; ::_thesis: (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] then M . i in (doms F) . i by A1, PBOOLE:def_1; then A3: M . i in dom (F . i) by A2, MSSUBFAM:14; A is_transformable_to [|B,C|] proof let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in I or not [|B,C|] . i = {} or A . i = {} ) assume i in I ; ::_thesis: ( not [|B,C|] . i = {} or A . i = {} ) hence ( not [|B,C|] . i = {} or A . i = {} ) ; ::_thesis: verum end; then M in A by A1, MSSUBFAM:17; then F .. M in [|B,C|] by CLOSURE1:3; then (F .. M) . i in [|B,C|] . i by A2, PBOOLE:def_1; then (F .. M) . i in [:(B . i),(C . i):] by A2, PBOOLE:def_16; then A4: (F . i) . (M . i) in [:(B . i),(C . i):] by A2, PRALG_1:def_18; set z = (F . i) . (M . i); (Mpr2 F) . i = pr2 (F . i) by A2, Def2; then A5: ((Mpr2 F) .. M) . i = (pr2 (F . i)) . (M . i) by A2, PRALG_1:def_18 .= ((F . i) . (M . i)) `2 by A3, MCART_1:def_13 ; (Mpr1 F) . i = pr1 (F . i) by A2, Def1; then ((Mpr1 F) .. M) . i = (pr1 (F . i)) . (M . i) by A2, PRALG_1:def_18 .= ((F . i) . (M . i)) `1 by A3, MCART_1:def_12 ; then (F . i) . (M . i) = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] by A4, A5, MCART_1:21; hence (F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)] by A2, PRALG_1:def_18; ::_thesis: verum end; begin registration let S be non empty ManySortedSign ; cluster the Sorts of (Trivial_Algebra S) -> V2() V32() ; coherence ( the Sorts of (Trivial_Algebra S) is finite-yielding & the Sorts of (Trivial_Algebra S) is non-empty ) proof ex A being ManySortedSet of the carrier of S st {A} = the carrier of S --> {0} by Th5; hence ( the Sorts of (Trivial_Algebra S) is finite-yielding & the Sorts of (Trivial_Algebra S) is non-empty ) by MSAFREE2:def_12; ::_thesis: verum end; end; registration let S be non empty ManySortedSign ; cluster Trivial_Algebra S -> non-empty finite-yielding ; coherence ( Trivial_Algebra S is finite-yielding & Trivial_Algebra S is non-empty ) proof thus the Sorts of (Trivial_Algebra S) is V32() ; :: according to MSAFREE2:def_11 ::_thesis: Trivial_Algebra S is non-empty let i be set ; :: according to MSUALG_1:def_3,PBOOLE:def_13 ::_thesis: ( not i in the carrier of S or not the Sorts of (Trivial_Algebra S) . i is empty ) assume i in the carrier of S ; ::_thesis: not the Sorts of (Trivial_Algebra S) . i is empty hence not the Sorts of (Trivial_Algebra S) . i is empty ; ::_thesis: verum end; end; theorem Th24: :: MSUALG_9:24 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for F being ManySortedFunction of A,(Trivial_Algebra S) for o being OperSymbol of S for x being Element of Args (o,A) holds ( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for F being ManySortedFunction of A,(Trivial_Algebra S) for o being OperSymbol of S for x being Element of Args (o,A) holds ( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 ) let A be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,(Trivial_Algebra S) for o being OperSymbol of S for x being Element of Args (o,A) holds ( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 ) let F be ManySortedFunction of A,(Trivial_Algebra S); ::_thesis: for o being OperSymbol of S for x being Element of Args (o,A) holds ( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 ) let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,A) holds ( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 ) let x be Element of Args (o,A); ::_thesis: ( (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 & (Den (o,(Trivial_Algebra S))) . (F # x) = 0 ) set I = the carrier of S; set SA = the Sorts of A; set T = Trivial_Algebra S; set ST = the Sorts of (Trivial_Algebra S); set r = the_result_sort_of o; consider i being set such that A1: i in the carrier of S and A2: Result (o,(Trivial_Algebra S)) = the Sorts of (Trivial_Algebra S) . i by PBOOLE:138; reconsider d = (Den (o,A)) . x as Element of the Sorts of A . (the_result_sort_of o) by FUNCT_2:15; consider XX being ManySortedSet of the carrier of S such that A3: {XX} = the carrier of S --> {0} by Th5; A4: the Sorts of (Trivial_Algebra S) = {XX} by A3, MSAFREE2:def_12; then A5: the Sorts of (Trivial_Algebra S) . (the_result_sort_of o) = {0} by A3, FUNCOP_1:7; thus (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = (F . (the_result_sort_of o)) . d .= 0 by A5, TARSKI:def_1 ; ::_thesis: (Den (o,(Trivial_Algebra S))) . (F # x) = 0 the Sorts of (Trivial_Algebra S) . i = {0} by A3, A4, A1, FUNCOP_1:7; hence (Den (o,(Trivial_Algebra S))) . (F # x) = 0 by A2, TARSKI:def_1; ::_thesis: verum end; theorem Th25: :: MSUALG_9:25 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S let A be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S let F be ManySortedFunction of A,(Trivial_Algebra S); ::_thesis: F is_epimorphism A, Trivial_Algebra S set I = the carrier of S; consider XX being ManySortedSet of the carrier of S such that A1: {XX} = the carrier of S --> {0} by Th5; thus F is_homomorphism A, Trivial_Algebra S :: according to MSUALG_3:def_8 ::_thesis: F is "onto" proof let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,A) = {} or for b1 being Element of Args (o,A) holds (F . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,(Trivial_Algebra S))) . (F # b1) ) assume Args (o,A) <> {} ; ::_thesis: for b1 being Element of Args (o,A) holds (F . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,(Trivial_Algebra S))) . (F # b1) let x be Element of Args (o,A); ::_thesis: (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,(Trivial_Algebra S))) . (F # x) thus (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = 0 by Th24 .= (Den (o,(Trivial_Algebra S))) . (F # x) by Th24 ; ::_thesis: verum end; the Sorts of (Trivial_Algebra S) = {XX} by A1, MSAFREE2:def_12; hence F is "onto" by Th9; ::_thesis: verum end; theorem :: MSUALG_9:26 for S being non empty non void ManySortedSign for A being MSAlgebra over S st ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} holds A, Trivial_Algebra S are_isomorphic proof let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S st ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} holds A, Trivial_Algebra S are_isomorphic let A be MSAlgebra over S; ::_thesis: ( ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} implies A, Trivial_Algebra S are_isomorphic ) assume A1: ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} ; ::_thesis: A, Trivial_Algebra S are_isomorphic set I = the carrier of S; set SB = the Sorts of A; set ST = the Sorts of (Trivial_Algebra S); consider X being ManySortedSet of the carrier of S such that A2: the Sorts of A = {X} by A1; set F = the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S); reconsider F1 = the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) as ManySortedFunction of {X}, the Sorts of (Trivial_Algebra S) by A2; take the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) ; :: according to MSUALG_3:def_11 ::_thesis: the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_isomorphism A, Trivial_Algebra S A is non-empty by A2, MSUALG_1:def_3; hence the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_epimorphism A, Trivial_Algebra S by Th25; :: according to MSUALG_3:def_10 ::_thesis: the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_monomorphism A, Trivial_Algebra S hence the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_homomorphism A, Trivial_Algebra S by MSUALG_3:def_8; :: according to MSUALG_3:def_9 ::_thesis: the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is "1-1" F1 is "1-1" by Th10; hence the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is "1-1" ; ::_thesis: verum end; begin theorem :: MSUALG_9:27 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|] proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|] let A be non-empty MSAlgebra over S; ::_thesis: for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|] let C be MSCongruence of A; ::_thesis: C is ManySortedSubset of [| the Sorts of A, the Sorts of A|] set SF = the Sorts of A; let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in the carrier of S or C . i c= [| the Sorts of A, the Sorts of A|] . i ) assume A1: i in the carrier of S ; ::_thesis: C . i c= [| the Sorts of A, the Sorts of A|] . i C . i is Relation of ( the Sorts of A . i),( the Sorts of A . i) by A1, MSUALG_4:def_1; then C . i c= [:( the Sorts of A . i),( the Sorts of A . i):] ; hence C . i c= [| the Sorts of A, the Sorts of A|] . i by A1, PBOOLE:def_16; ::_thesis: verum end; theorem :: MSUALG_9:28 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being Subset of (CongrLatt A) for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds meet |:F:| is MSCongruence of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being Subset of (CongrLatt A) for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds meet |:F:| is MSCongruence of A let A be non-empty MSAlgebra over S; ::_thesis: for R being Subset of (CongrLatt A) for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds meet |:F:| is MSCongruence of A let R be Subset of (CongrLatt A); ::_thesis: for F being SubsetFamily of [| the Sorts of A, the Sorts of A|] st R = F holds meet |:F:| is MSCongruence of A let F be SubsetFamily of [| the Sorts of A, the Sorts of A|]; ::_thesis: ( R = F implies meet |:F:| is MSCongruence of A ) assume A1: R = F ; ::_thesis: meet |:F:| is MSCongruence of A set R0 = meet |:F:|; set SF = the Sorts of A; set I = the carrier of S; percases ( not F is empty or F is empty ) ; suppose not F is empty ; ::_thesis: meet |:F:| is MSCongruence of A then reconsider F1 = F as non empty SubsetFamily of [| the Sorts of A, the Sorts of A|] ; A2: F1 c= the carrier of (EqRelLatt the Sorts of A) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in F1 or q in the carrier of (EqRelLatt the Sorts of A) ) assume q in F1 ; ::_thesis: q in the carrier of (EqRelLatt the Sorts of A) then q is MSCongruence of A by A1, MSUALG_5:def_6; hence q in the carrier of (EqRelLatt the Sorts of A) by MSUALG_5:def_5; ::_thesis: verum end; then A3: meet |:F:| is MSEquivalence_Relation-like ManySortedRelation of the Sorts of A by MSUALG_7:8; reconsider R0 = meet |:F:| as ManySortedRelation of A by A2, MSUALG_7:8; R0 is MSEquivalence-like proof let i be set ; :: according to MSUALG_4:def_2,MSUALG_4:def_3 ::_thesis: for b1 being Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] holds ( not i in the carrier of S or not R0 . i = b1 or b1 is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] ) let R be Relation of ( the Sorts of A . i); ::_thesis: ( not i in the carrier of S or not R0 . i = R or R is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] ) assume ( i in the carrier of S & R0 . i = R ) ; ::_thesis: R is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] hence R is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] by A3, MSUALG_4:def_2; ::_thesis: verum end; then reconsider R0 = R0 as MSEquivalence-like ManySortedRelation of A ; now__::_thesis:_for_o_being_OperSymbol_of_S for_a,_b_being_Element_of_Args_(o,A)_st_(_for_n_being_Nat_st_n_in_dom_a_holds_ [(a_._n),(b_._n)]_in_R0_._((the_arity_of_o)_/._n)_)_holds_ [((Den_(o,A))_._a),((Den_(o,A))_._b)]_in_R0_._(the_result_sort_of_o) let o be OperSymbol of S; ::_thesis: for a, b being Element of Args (o,A) st ( for n being Nat st n in dom a holds [(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o) let a, b be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom a holds [(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o) ) assume A4: for n being Nat st n in dom a holds [(a . n),(b . n)] in R0 . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o) set r = the_result_sort_of o; consider Q being Subset-Family of ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of o)) such that A5: Q = |:F1:| . (the_result_sort_of o) and A6: R0 . (the_result_sort_of o) = Intersect Q by MSSUBFAM:def_1; A7: Q = { (s . (the_result_sort_of o)) where s is Element of Bool [| the Sorts of A, the Sorts of A|] : s in F1 } by A5, CLOSURE2:14; now__::_thesis:_for_Y_being_set_st_Y_in_Q_holds_ [((Den_(o,A))_._a),((Den_(o,A))_._b)]_in_Y let Y be set ; ::_thesis: ( Y in Q implies [((Den (o,A)) . a),((Den (o,A)) . b)] in Y ) assume Y in Q ; ::_thesis: [((Den (o,A)) . a),((Den (o,A)) . b)] in Y then consider s being Element of Bool [| the Sorts of A, the Sorts of A|] such that A8: Y = s . (the_result_sort_of o) and A9: s in F1 by A7; reconsider s = s as MSCongruence of A by A1, A9, MSUALG_5:def_6; now__::_thesis:_for_n_being_Nat_st_n_in_dom_a_holds_ [(a_._n),(b_._n)]_in_s_._((the_arity_of_o)_/._n) let n be Nat; ::_thesis: ( n in dom a implies [(a . n),(b . n)] in s . ((the_arity_of o) /. n) ) assume A10: n in dom a ; ::_thesis: [(a . n),(b . n)] in s . ((the_arity_of o) /. n) set t = (the_arity_of o) /. n; consider G being Subset-Family of ([| the Sorts of A, the Sorts of A|] . ((the_arity_of o) /. n)) such that A11: G = |:F1:| . ((the_arity_of o) /. n) and A12: R0 . ((the_arity_of o) /. n) = Intersect G by MSSUBFAM:def_1; G = { (j . ((the_arity_of o) /. n)) where j is Element of Bool [| the Sorts of A, the Sorts of A|] : j in F1 } by A11, CLOSURE2:14; then A13: s . ((the_arity_of o) /. n) in G by A9; [(a . n),(b . n)] in Intersect G by A4, A10, A12; then [(a . n),(b . n)] in meet G by A11, SETFAM_1:def_9; hence [(a . n),(b . n)] in s . ((the_arity_of o) /. n) by A13, SETFAM_1:def_1; ::_thesis: verum end; hence [((Den (o,A)) . a),((Den (o,A)) . b)] in Y by A8, MSUALG_4:def_4; ::_thesis: verum end; then [((Den (o,A)) . a),((Den (o,A)) . b)] in meet Q by A5, SETFAM_1:def_1; hence [((Den (o,A)) . a),((Den (o,A)) . b)] in R0 . (the_result_sort_of o) by A5, A6, SETFAM_1:def_9; ::_thesis: verum end; hence meet |:F:| is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum end; suppose F is empty ; ::_thesis: meet |:F:| is MSCongruence of A then |:F:| = [[0]] the carrier of S by CLOSURE2:def_3; then meet |:F:| = [| the Sorts of A, the Sorts of A|] by MSSUBFAM:41; hence meet |:F:| is MSCongruence of A by MSUALG_5:18; ::_thesis: verum end; end; end; theorem :: MSUALG_9:29 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for C being MSCongruence of A st C = [| the Sorts of A, the Sorts of A|] holds the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A} proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for C being MSCongruence of A st C = [| the Sorts of A, the Sorts of A|] holds the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A} let A be non-empty MSAlgebra over S; ::_thesis: for C being MSCongruence of A st C = [| the Sorts of A, the Sorts of A|] holds the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A} let C be MSCongruence of A; ::_thesis: ( C = [| the Sorts of A, the Sorts of A|] implies the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A} ) assume A1: C = [| the Sorts of A, the Sorts of A|] ; ::_thesis: the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A} now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ the_Sorts_of_(QuotMSAlg_(A,C))_._i_=_{_the_Sorts_of_A}_._i let i be set ; ::_thesis: ( i in the carrier of S implies the Sorts of (QuotMSAlg (A,C)) . i = { the Sorts of A} . i ) assume i in the carrier of S ; ::_thesis: the Sorts of (QuotMSAlg (A,C)) . i = { the Sorts of A} . i then reconsider s = i as Element of S ; A2: C . s = [:( the Sorts of A . s),( the Sorts of A . s):] by A1, PBOOLE:def_16 .= nabla ( the Sorts of A . s) by EQREL_1:def_1 ; thus the Sorts of (QuotMSAlg (A,C)) . i = Class (C . s) by MSUALG_4:def_6 .= {( the Sorts of A . s)} by A2, Th4 .= { the Sorts of A} . i by PZFMISC1:def_1 ; ::_thesis: verum end; hence the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A} by PBOOLE:3; ::_thesis: verum end; theorem Th30: :: MSUALG_9:30 for S being non empty non void ManySortedSign for A, B being non-empty MSAlgebra over S for F being ManySortedFunction of A,B st F is_homomorphism A,B holds (MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F proof let S be non empty non void ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over S for F being ManySortedFunction of A,B st F is_homomorphism A,B holds (MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F let A, B be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,B st F is_homomorphism A,B holds (MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F let F be ManySortedFunction of A,B; ::_thesis: ( F is_homomorphism A,B implies (MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F ) assume A1: F is_homomorphism A,B ; ::_thesis: (MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ ((MSHomQuot_F)_**_(MSNat_Hom_(A,(MSCng_F))))_._i_=_F_._i let i be set ; ::_thesis: ( i in the carrier of S implies ((MSHomQuot F) ** (MSNat_Hom (A,(MSCng F)))) . i = F . i ) assume i in the carrier of S ; ::_thesis: ((MSHomQuot F) ** (MSNat_Hom (A,(MSCng F)))) . i = F . i then reconsider s = i as SortSymbol of S ; reconsider h = MSHomQuot (F,s) as Function of ((Class (MSCng F)) . s),( the Sorts of B . s) ; reconsider f = h * (MSNat_Hom (A,(MSCng F),s)) as Function of ( the Sorts of A . s),( the Sorts of B . s) ; A2: for c being Element of the Sorts of A . s holds f . c = (F . s) . c proof let c be Element of the Sorts of A . s; ::_thesis: f . c = (F . s) . c thus f . c = h . ((MSNat_Hom (A,(MSCng F),s)) . c) by FUNCT_2:15 .= h . (Class (((MSCng F) . s),c)) by MSUALG_4:def_15 .= h . (Class ((MSCng (F,s)),c)) by A1, MSUALG_4:def_18 .= (F . s) . c by A1, MSUALG_4:def_19 ; ::_thesis: verum end; thus ((MSHomQuot F) ** (MSNat_Hom (A,(MSCng F)))) . i = ((MSHomQuot F) . s) * ((MSNat_Hom (A,(MSCng F))) . s) by MSUALG_3:2 .= (MSHomQuot (F,s)) * ((MSNat_Hom (A,(MSCng F))) . s) by MSUALG_4:def_20 .= (MSHomQuot (F,s)) * (MSNat_Hom (A,(MSCng F),s)) by MSUALG_4:def_16 .= F . i by A2, FUNCT_2:63 ; ::_thesis: verum end; hence (MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F by PBOOLE:3; ::_thesis: verum end; theorem Th31: :: MSUALG_9:31 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for C being MSCongruence of A for s being SortSymbol of S for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for C being MSCongruence of A for s being SortSymbol of S for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x) let A be non-empty MSAlgebra over S; ::_thesis: for C being MSCongruence of A for s being SortSymbol of S for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x) let C be MSCongruence of A; ::_thesis: for s being SortSymbol of S for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x) let s be SortSymbol of S; ::_thesis: for a being Element of the Sorts of (QuotMSAlg (A,C)) . s ex x being Element of the Sorts of A . s st a = Class (C,x) let a be Element of the Sorts of (QuotMSAlg (A,C)) . s; ::_thesis: ex x being Element of the Sorts of A . s st a = Class (C,x) a in (Class C) . s ; then a in Class (C . s) by MSUALG_4:def_6; then consider t being set such that A1: t in the Sorts of A . s and A2: a = Class ((C . s),t) by EQREL_1:def_3; reconsider t = t as Element of the Sorts of A . s by A1; take t ; ::_thesis: a = Class (C,t) thus a = Class (C,t) by A2; ::_thesis: verum end; theorem :: MSUALG_9:32 for S being non empty non void ManySortedSign for A being MSAlgebra over S for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds for i being Element of S for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds ( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds for i being Element of S for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds ( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) ) let A be MSAlgebra over S; ::_thesis: for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds for i being Element of S for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds ( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) ) let C1, C2 be MSEquivalence-like ManySortedRelation of A; ::_thesis: ( C1 c= C2 implies for i being Element of S for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds ( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) ) ) assume A1: C1 c= C2 ; ::_thesis: for i being Element of S for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds ( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) ) let i be Element of S; ::_thesis: for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds ( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) ) let x, y be Element of the Sorts of A . i; ::_thesis: ( [x,y] in C1 . i implies ( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) ) ) assume A2: [x,y] in C1 . i ; ::_thesis: ( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) ) field (C1 . i) = the Sorts of A . i by ORDERS_1:12; then A3: C1 . i is_transitive_in the Sorts of A . i by RELAT_2:def_16; A4: C1 . i c= C2 . i by A1, PBOOLE:def_2; thus Class (C1,x) c= Class (C2,y) ::_thesis: ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Class (C1,x) or q in Class (C2,y) ) assume A5: q in Class (C1,x) ; ::_thesis: q in Class (C2,y) then [q,x] in C1 . i by EQREL_1:19; then [q,y] in C1 . i by A2, A3, A5, RELAT_2:def_8; hence q in Class (C2,y) by A4, EQREL_1:19; ::_thesis: verum end; assume A is non-empty ; ::_thesis: Class (C1,y) c= Class (C2,x) then reconsider B = A as non-empty MSAlgebra over S ; field (C1 . i) = the Sorts of A . i by ORDERS_1:12; then C1 . i is_symmetric_in the Sorts of B . i by RELAT_2:def_11; then A6: [y,x] in C1 . i by A2, RELAT_2:def_3; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Class (C1,y) or q in Class (C2,x) ) assume A7: q in Class (C1,y) ; ::_thesis: q in Class (C2,x) [q,y] in C1 . i by A7, EQREL_1:19; then [q,x] in C1 . i by A3, A7, A6, RELAT_2:def_8; hence q in Class (C2,x) by A4, EQREL_1:19; ::_thesis: verum end; theorem :: MSUALG_9:33 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for C being MSCongruence of A for s being SortSymbol of S for x, y being Element of the Sorts of A . s holds ( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for C being MSCongruence of A for s being SortSymbol of S for x, y being Element of the Sorts of A . s holds ( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s ) let A be non-empty MSAlgebra over S; ::_thesis: for C being MSCongruence of A for s being SortSymbol of S for x, y being Element of the Sorts of A . s holds ( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s ) let C be MSCongruence of A; ::_thesis: for s being SortSymbol of S for x, y being Element of the Sorts of A . s holds ( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s ) let s be SortSymbol of S; ::_thesis: for x, y being Element of the Sorts of A . s holds ( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s ) let x, y be Element of the Sorts of A . s; ::_thesis: ( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s ) set f = (MSNat_Hom (A,C)) . s; set g = MSNat_Hom (A,C,s); A1: (MSNat_Hom (A,C)) . s = MSNat_Hom (A,C,s) by MSUALG_4:def_16; hereby ::_thesis: ( [x,y] in C . s implies ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y ) assume A2: ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y ; ::_thesis: [x,y] in C . s Class ((C . s),x) = (MSNat_Hom (A,C,s)) . x by MSUALG_4:def_15 .= Class ((C . s),y) by A1, A2, MSUALG_4:def_15 ; hence [x,y] in C . s by EQREL_1:35; ::_thesis: verum end; assume A3: [x,y] in C . s ; ::_thesis: ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y thus ((MSNat_Hom (A,C)) . s) . x = Class ((C . s),x) by A1, MSUALG_4:def_15 .= Class ((C . s),y) by A3, EQREL_1:35 .= ((MSNat_Hom (A,C)) . s) . y by A1, MSUALG_4:def_15 ; ::_thesis: verum end; Lm1: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_ for_A_being_non-empty_MSAlgebra_over_S for_C1,_C2_being_MSCongruence_of_A for_G_being_ManySortedFunction_of_(QuotMSAlg_(A,C1)),(QuotMSAlg_(A,C2))_st_(_for_i_being_Element_of_S for_x_being_Element_of_the_Sorts_of_(QuotMSAlg_(A,C1))_._i for_xx_being_Element_of_the_Sorts_of_A_._i_st_x_=_Class_(C1,xx)_holds_ (G_._i)_._x_=_Class_(C2,xx)_)_holds_ G_is_"onto" let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for C1, C2 being MSCongruence of A for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) holds G is "onto" let A be non-empty MSAlgebra over S; ::_thesis: for C1, C2 being MSCongruence of A for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) holds G is "onto" let C1, C2 be MSCongruence of A; ::_thesis: for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) holds G is "onto" let G be ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)); ::_thesis: ( ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) implies G is "onto" ) assume A1: for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ; ::_thesis: G is "onto" thus G is "onto" ::_thesis: verum proof let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in the carrier of S or rng (G . i) = the Sorts of (QuotMSAlg (A,C2)) . i ) set sL = the Sorts of (QuotMSAlg (A,C1)); set sP = the Sorts of (QuotMSAlg (A,C2)); assume i in the carrier of S ; ::_thesis: rng (G . i) = the Sorts of (QuotMSAlg (A,C2)) . i then reconsider s = i as SortSymbol of S ; A2: dom (G . s) = the Sorts of (QuotMSAlg (A,C1)) . s by FUNCT_2:def_1; rng (G . s) c= the Sorts of (QuotMSAlg (A,C2)) . s ; hence rng (G . i) c= the Sorts of (QuotMSAlg (A,C2)) . i ; :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of (QuotMSAlg (A,C2)) . i c= rng (G . i) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the Sorts of (QuotMSAlg (A,C2)) . i or q in rng (G . i) ) assume q in the Sorts of (QuotMSAlg (A,C2)) . i ; ::_thesis: q in rng (G . i) then q in Class (C2 . s) by MSUALG_4:def_6; then consider a being set such that A3: a in the Sorts of A . s and A4: q = Class ((C2 . s),a) by EQREL_1:def_3; reconsider a = a as Element of the Sorts of A . s by A3; Class ((C1 . s),a) in Class (C1 . s) by EQREL_1:def_3; then reconsider x = Class (C1,a) as Element of the Sorts of (QuotMSAlg (A,C1)) . s by MSUALG_4:def_6; (G . s) . x = Class (C2,a) by A1 .= Class ((C2 . s),a) ; hence q in rng (G . i) by A4, A2, FUNCT_1:def_3; ::_thesis: verum end; end; theorem Th34: :: MSUALG_9:34 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for C1, C2 being MSCongruence of A for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) holds G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for C1, C2 being MSCongruence of A for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) holds G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) let A be non-empty MSAlgebra over S; ::_thesis: for C1, C2 being MSCongruence of A for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) holds G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) let C1, C2 be MSCongruence of A; ::_thesis: for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) holds G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) set sL = the Sorts of (QuotMSAlg (A,C1)); let G be ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)); ::_thesis: ( ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) implies G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) ) assume A1: for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ; ::_thesis: G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ (G_**_(MSNat_Hom_(A,C1)))_._i_=_(MSNat_Hom_(A,C2))_._i let i be set ; ::_thesis: ( i in the carrier of S implies (G ** (MSNat_Hom (A,C1))) . i = (MSNat_Hom (A,C2)) . i ) assume i in the carrier of S ; ::_thesis: (G ** (MSNat_Hom (A,C1))) . i = (MSNat_Hom (A,C2)) . i then reconsider s = i as SortSymbol of S ; A2: for c being Element of the Sorts of A . s holds ((G . s) * ((MSNat_Hom (A,C1)) . s)) . c = ((MSNat_Hom (A,C2)) . s) . c proof let c be Element of the Sorts of A . s; ::_thesis: ((G . s) * ((MSNat_Hom (A,C1)) . s)) . c = ((MSNat_Hom (A,C2)) . s) . c Class ((C1 . s),c) in Class (C1 . s) by EQREL_1:def_3; then A3: Class (C1,c) is Element of the Sorts of (QuotMSAlg (A,C1)) . s by MSUALG_4:def_6; thus ((G . s) * ((MSNat_Hom (A,C1)) . s)) . c = (G . s) . (((MSNat_Hom (A,C1)) . s) . c) by FUNCT_2:15 .= (G . s) . ((MSNat_Hom (A,C1,s)) . c) by MSUALG_4:def_16 .= (G . s) . (Class (C1,c)) by MSUALG_4:def_15 .= Class (C2,c) by A1, A3 .= (MSNat_Hom (A,C2,s)) . c by MSUALG_4:def_15 .= ((MSNat_Hom (A,C2)) . s) . c by MSUALG_4:def_16 ; ::_thesis: verum end; thus (G ** (MSNat_Hom (A,C1))) . i = (G . s) * ((MSNat_Hom (A,C1)) . s) by MSUALG_3:2 .= (MSNat_Hom (A,C2)) . i by A2, FUNCT_2:63 ; ::_thesis: verum end; hence G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) by PBOOLE:3; ::_thesis: verum end; theorem Th35: :: MSUALG_9:35 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for C1, C2 being MSCongruence of A for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) holds G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for C1, C2 being MSCongruence of A for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) holds G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) let A be non-empty MSAlgebra over S; ::_thesis: for C1, C2 being MSCongruence of A for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) holds G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) let C1, C2 be MSCongruence of A; ::_thesis: for G being ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)) st ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) holds G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) MSNat_Hom (A,C2) is_epimorphism A, QuotMSAlg (A,C2) by MSUALG_4:3; then A1: MSNat_Hom (A,C2) is_homomorphism A, QuotMSAlg (A,C2) by MSUALG_3:def_8; let G be ManySortedFunction of (QuotMSAlg (A,C1)),(QuotMSAlg (A,C2)); ::_thesis: ( ( for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ) implies G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) ) assume A2: for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (G . i) . x = Class (C2,xx) ; ::_thesis: G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) by A2, Th34; hence G is_homomorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) by A1, Th19, MSUALG_4:3; :: according to MSUALG_3:def_8 ::_thesis: G is "onto" thus G is "onto" by A2, Lm1; ::_thesis: verum end; theorem :: MSUALG_9:36 for S being non empty non void ManySortedSign for A, B being non-empty MSAlgebra over S for F being ManySortedFunction of A,B st F is_homomorphism A,B holds for C1 being MSCongruence of A st C1 c= MSCng F holds ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st ( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A, B being non-empty MSAlgebra over S for F being ManySortedFunction of A,B st F is_homomorphism A,B holds for C1 being MSCongruence of A st C1 c= MSCng F holds ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st ( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) ) let A, B be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of A,B st F is_homomorphism A,B holds for C1 being MSCongruence of A st C1 c= MSCng F holds ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st ( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) ) let F be ManySortedFunction of A,B; ::_thesis: ( F is_homomorphism A,B implies for C1 being MSCongruence of A st C1 c= MSCng F holds ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st ( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) ) ) assume A1: F is_homomorphism A,B ; ::_thesis: for C1 being MSCongruence of A st C1 c= MSCng F holds ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st ( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) ) MSHomQuot F is_monomorphism QuotMSAlg (A,(MSCng F)),B by A1, MSUALG_4:4; then A2: MSHomQuot F is_homomorphism QuotMSAlg (A,(MSCng F)),B by MSUALG_3:def_9; let C1 be MSCongruence of A; ::_thesis: ( C1 c= MSCng F implies ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st ( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) ) ) assume A3: C1 c= MSCng F ; ::_thesis: ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st ( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) ) set G = MSNat_Hom (A,C1); set I = the carrier of S; set sQ = the Sorts of (QuotMSAlg (A,C1)); set sF = the Sorts of (QuotMSAlg (A,(MSCng F))); defpred S1[ set , set , set ] means ex s being Element of the carrier of S ex xx being Element of the Sorts of A . s st ( \$3 = s & \$2 = Class (C1,xx) & \$1 = Class ((MSCng F),xx) ); A4: for i being set st i in the carrier of S holds for x being set st x in the Sorts of (QuotMSAlg (A,C1)) . i holds ex y being set st ( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] ) proof let i be set ; ::_thesis: ( i in the carrier of S implies for x being set st x in the Sorts of (QuotMSAlg (A,C1)) . i holds ex y being set st ( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] ) ) assume i in the carrier of S ; ::_thesis: for x being set st x in the Sorts of (QuotMSAlg (A,C1)) . i holds ex y being set st ( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] ) then reconsider s = i as Element of the carrier of S ; let x be set ; ::_thesis: ( x in the Sorts of (QuotMSAlg (A,C1)) . i implies ex y being set st ( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] ) ) assume x in the Sorts of (QuotMSAlg (A,C1)) . i ; ::_thesis: ex y being set st ( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] ) then consider x1 being Element of the Sorts of A . s such that A5: x = Class (C1,x1) by Th31; take y = Class ((MSCng F),x1); ::_thesis: ( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S1[y,x,i] ) y in Class ((MSCng F) . s) by EQREL_1:def_3; hence y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i by MSUALG_4:def_6; ::_thesis: S1[y,x,i] thus S1[y,x,i] by A5; ::_thesis: verum end; consider C12 being ManySortedFunction of the Sorts of (QuotMSAlg (A,C1)), the Sorts of (QuotMSAlg (A,(MSCng F))) such that A6: for i being set st i in the carrier of S holds ex f being Function of ( the Sorts of (QuotMSAlg (A,C1)) . i),( the Sorts of (QuotMSAlg (A,(MSCng F))) . i) st ( f = C12 . i & ( for x being set st x in the Sorts of (QuotMSAlg (A,C1)) . i holds S1[f . x,x,i] ) ) from MSSUBFAM:sch_1(A4); reconsider H = (MSHomQuot F) ** C12 as ManySortedFunction of (QuotMSAlg (A,C1)),B ; take H ; ::_thesis: ( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) ) A7: for i being Element of S for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (C12 . i) . x = Class ((MSCng F),xx) proof let i be Element of S; ::_thesis: for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (C12 . i) . x = Class ((MSCng F),xx) let x be Element of the Sorts of (QuotMSAlg (A,C1)) . i; ::_thesis: for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds (C12 . i) . x = Class ((MSCng F),xx) let xx be Element of the Sorts of A . i; ::_thesis: ( x = Class (C1,xx) implies (C12 . i) . x = Class ((MSCng F),xx) ) assume A8: x = Class (C1,xx) ; ::_thesis: (C12 . i) . x = Class ((MSCng F),xx) consider f being Function of ( the Sorts of (QuotMSAlg (A,C1)) . i),( the Sorts of (QuotMSAlg (A,(MSCng F))) . i) such that A9: f = C12 . i and A10: for x being set st x in the Sorts of (QuotMSAlg (A,C1)) . i holds S1[f . x,x,i] by A6; consider s being Element of the carrier of S, x1 being Element of the Sorts of A . s such that A11: i = s and A12: x = Class (C1,x1) and A13: f . x = Class ((MSCng F),x1) by A10; xx in Class ((C1 . s),x1) by A8, A12, EQREL_1:23; then A14: [xx,x1] in C1 . s by EQREL_1:19; C1 . s c= (MSCng F) . s by A3, PBOOLE:def_2; then xx in Class (((MSCng F) . s),x1) by A14, EQREL_1:19; hence (C12 . i) . x = Class ((MSCng F),xx) by A9, A11, A13, EQREL_1:23; ::_thesis: verum end; then C12 is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,(MSCng F)) by Th35; then C12 is_homomorphism QuotMSAlg (A,C1), QuotMSAlg (A,(MSCng F)) by MSUALG_3:def_8; hence H is_homomorphism QuotMSAlg (A,C1),B by A2, MSUALG_3:10; ::_thesis: F = H ** (MSNat_Hom (A,C1)) A15: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ (C12_**_(MSNat_Hom_(A,C1)))_._i_=_(MSNat_Hom_(A,(MSCng_F)))_._i let i be set ; ::_thesis: ( i in the carrier of S implies (C12 ** (MSNat_Hom (A,C1))) . i = (MSNat_Hom (A,(MSCng F))) . i ) assume i in the carrier of S ; ::_thesis: (C12 ** (MSNat_Hom (A,C1))) . i = (MSNat_Hom (A,(MSCng F))) . i then reconsider s = i as SortSymbol of S ; A16: for x being Element of the Sorts of A . s holds ((C12 . s) * ((MSNat_Hom (A,C1)) . s)) . x = ((MSNat_Hom (A,(MSCng F))) . s) . x proof let x be Element of the Sorts of A . s; ::_thesis: ((C12 . s) * ((MSNat_Hom (A,C1)) . s)) . x = ((MSNat_Hom (A,(MSCng F))) . s) . x Class ((C1 . s),x) in Class (C1 . s) by EQREL_1:def_3; then A17: Class (C1,x) in (Class C1) . s by MSUALG_4:def_6; thus ((C12 . s) * ((MSNat_Hom (A,C1)) . s)) . x = (C12 . s) . (((MSNat_Hom (A,C1)) . s) . x) by FUNCT_2:15 .= (C12 . s) . ((MSNat_Hom (A,C1,s)) . x) by MSUALG_4:def_16 .= (C12 . s) . (Class (C1,x)) by MSUALG_4:def_15 .= Class ((MSCng F),x) by A7, A17 .= (MSNat_Hom (A,(MSCng F),s)) . x by MSUALG_4:def_15 .= ((MSNat_Hom (A,(MSCng F))) . s) . x by MSUALG_4:def_16 ; ::_thesis: verum end; thus (C12 ** (MSNat_Hom (A,C1))) . i = (C12 . s) * ((MSNat_Hom (A,C1)) . s) by MSUALG_3:2 .= (MSNat_Hom (A,(MSCng F))) . i by A16, FUNCT_2:63 ; ::_thesis: verum end; thus F = (MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) by A1, Th30 .= (MSHomQuot F) ** (C12 ** (MSNat_Hom (A,C1))) by A15, PBOOLE:3 .= H ** (MSNat_Hom (A,C1)) by PBOOLE:140 ; ::_thesis: verum end;