:: MSUALG_6 semantic presentation begin definition let S be non empty ManySortedSign ; let A be MSAlgebra over S; let s be SortSymbol of S; mode Element of A,s is Element of the Sorts of A . s; end; definition let I be set ; let A be ManySortedSet of I; let h1, h2 be ManySortedFunction of A,A; :: original: ** redefine funch2 ** h1 -> ManySortedFunction of A,A; coherence h2 ** h1 is ManySortedFunction of A,A proof set h = h2 ** h1; A1: dom h2 = I by PARTFUN1:def_2; dom h1 = I by PARTFUN1:def_2; then A2: dom (h2 ** h1) = I /\ I by A1, PBOOLE:def_19 .= I ; then reconsider h = h2 ** h1 as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; h is ManySortedFunction of A,A proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or h . i is Element of bool [:(A . i),(A . i):] ) assume A3: i in I ; ::_thesis: h . i is Element of bool [:(A . i),(A . i):] then reconsider f = h1 . i, g = h2 . i as Function of (A . i),(A . i) by PBOOLE:def_15; h . i = g * f by A2, A3, PBOOLE:def_19; hence h . i is Element of bool [:(A . i),(A . i):] ; ::_thesis: verum end; hence h2 ** h1 is ManySortedFunction of A,A ; ::_thesis: verum end; end; theorem Th1: :: MSUALG_6:1 for S being non empty non void ManySortedSign for A being MSAlgebra over S for o being OperSymbol of S for a being set st a in Args (o,A) holds a is Function proof let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S for o being OperSymbol of S for a being set st a in Args (o,A) holds a is Function let A be MSAlgebra over S; ::_thesis: for o being OperSymbol of S for a being set st a in Args (o,A) holds a is Function let o be OperSymbol of S; ::_thesis: for a being set st a in Args (o,A) holds a is Function let x be set ; ::_thesis: ( x in Args (o,A) implies x is Function ) assume x in Args (o,A) ; ::_thesis: x is Function then x in product ( the Sorts of A * (the_arity_of o)) by PRALG_2:3; then ex f being Function st ( x = f & dom f = dom ( the Sorts of A * (the_arity_of o)) & ( for y being set st y in dom ( the Sorts of A * (the_arity_of o)) holds f . y in ( the Sorts of A * (the_arity_of o)) . y ) ) by CARD_3:def_5; hence x is Function ; ::_thesis: verum end; theorem Th2: :: MSUALG_6:2 for S being non empty non void ManySortedSign for A being MSAlgebra over S for o being OperSymbol of S for a being Function st a in Args (o,A) holds ( dom a = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds a . i in the Sorts of A . ((the_arity_of o) /. i) ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S for o being OperSymbol of S for a being Function st a in Args (o,A) holds ( dom a = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds a . i in the Sorts of A . ((the_arity_of o) /. i) ) ) let A be MSAlgebra over S; ::_thesis: for o being OperSymbol of S for a being Function st a in Args (o,A) holds ( dom a = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds a . i in the Sorts of A . ((the_arity_of o) /. i) ) ) let o be OperSymbol of S; ::_thesis: for a being Function st a in Args (o,A) holds ( dom a = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds a . i in the Sorts of A . ((the_arity_of o) /. i) ) ) let x be Function; ::_thesis: ( x in Args (o,A) implies ( dom x = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds x . i in the Sorts of A . ((the_arity_of o) /. i) ) ) ) assume x in Args (o,A) ; ::_thesis: ( dom x = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds x . i in the Sorts of A . ((the_arity_of o) /. i) ) ) then x in product ( the Sorts of A * (the_arity_of o)) by PRALG_2:3; then A1: ex f being Function st ( x = f & dom f = dom ( the Sorts of A * (the_arity_of o)) & ( for y being set st y in dom ( the Sorts of A * (the_arity_of o)) holds f . y in ( the Sorts of A * (the_arity_of o)) . y ) ) by CARD_3:def_5; hence A2: dom x = dom (the_arity_of o) by PARTFUN1:def_2; ::_thesis: for i being set st i in dom (the_arity_of o) holds x . i in the Sorts of A . ((the_arity_of o) /. i) let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies x . y in the Sorts of A . ((the_arity_of o) /. y) ) assume A3: y in dom (the_arity_of o) ; ::_thesis: x . y in the Sorts of A . ((the_arity_of o) /. y) then A4: (the_arity_of o) . y = (the_arity_of o) /. y by PARTFUN1:def_6; x . y in ( the Sorts of A * (the_arity_of o)) . y by A1, A2, A3; hence x . y in the Sorts of A . ((the_arity_of o) /. y) by A3, A4, FUNCT_1:13; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; attrA is feasible means :Def1: :: MSUALG_6:def 1 for o being OperSymbol of S st Args (o,A) <> {} holds Result (o,A) <> {} ; end; :: deftheorem Def1 defines feasible MSUALG_6:def_1_:_ for S being non empty non void ManySortedSign for A being MSAlgebra over S holds ( A is feasible iff for o being OperSymbol of S st Args (o,A) <> {} holds Result (o,A) <> {} ); theorem Th3: :: MSUALG_6:3 for S being non empty non void ManySortedSign for o being OperSymbol of S for A being MSAlgebra over S holds ( Args (o,A) <> {} iff for i being Element of NAT st i in dom (the_arity_of o) holds the Sorts of A . ((the_arity_of o) /. i) <> {} ) proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for A being MSAlgebra over S holds ( Args (o,A) <> {} iff for i being Element of NAT st i in dom (the_arity_of o) holds the Sorts of A . ((the_arity_of o) /. i) <> {} ) let o be OperSymbol of S; ::_thesis: for A being MSAlgebra over S holds ( Args (o,A) <> {} iff for i being Element of NAT st i in dom (the_arity_of o) holds the Sorts of A . ((the_arity_of o) /. i) <> {} ) let A be MSAlgebra over S; ::_thesis: ( Args (o,A) <> {} iff for i being Element of NAT st i in dom (the_arity_of o) holds the Sorts of A . ((the_arity_of o) /. i) <> {} ) A1: dom ( the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3; A2: Args (o,A) = product ( the Sorts of A * (the_arity_of o)) by PRALG_2:3; hereby ::_thesis: ( ( for i being Element of NAT st i in dom (the_arity_of o) holds the Sorts of A . ((the_arity_of o) /. i) <> {} ) implies Args (o,A) <> {} ) assume A3: Args (o,A) <> {} ; ::_thesis: for i being Element of NAT st i in dom (the_arity_of o) holds the Sorts of A . ((the_arity_of o) /. i) <> {} let i be Element of NAT ; ::_thesis: ( i in dom (the_arity_of o) implies the Sorts of A . ((the_arity_of o) /. i) <> {} ) assume A4: i in dom (the_arity_of o) ; ::_thesis: the Sorts of A . ((the_arity_of o) /. i) <> {} then A5: the Sorts of A . ((the_arity_of o) . i) = ( the Sorts of A * (the_arity_of o)) . i by FUNCT_1:13; A6: (the_arity_of o) /. i = (the_arity_of o) . i by A4, PARTFUN1:def_6; ( the Sorts of A * (the_arity_of o)) . i in rng ( the Sorts of A * (the_arity_of o)) by A1, A4, FUNCT_1:def_3; hence the Sorts of A . ((the_arity_of o) /. i) <> {} by A2, A3, A5, A6, CARD_3:26; ::_thesis: verum end; assume A7: for i being Element of NAT st i in dom (the_arity_of o) holds the Sorts of A . ((the_arity_of o) /. i) <> {} ; ::_thesis: Args (o,A) <> {} assume Args (o,A) = {} ; ::_thesis: contradiction then {} in rng ( the Sorts of A * (the_arity_of o)) by A2, CARD_3:26; then consider x being set such that A8: x in dom (the_arity_of o) and A9: {} = ( the Sorts of A * (the_arity_of o)) . x by A1, FUNCT_1:def_3; reconsider x = x as Element of NAT by A8; A10: (the_arity_of o) /. x = (the_arity_of o) . x by A8, PARTFUN1:def_6; the Sorts of A . ((the_arity_of o) /. x) <> {} by A7, A8; hence contradiction by A8, A9, A10, FUNCT_1:13; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; cluster non-empty -> feasible for MSAlgebra over S; coherence for b1 being MSAlgebra over S st b1 is non-empty holds b1 is feasible proof let A be MSAlgebra over S; ::_thesis: ( A is non-empty implies A is feasible ) assume A is non-empty ; ::_thesis: A is feasible then reconsider B = A as non-empty MSAlgebra over S ; let o be OperSymbol of S; :: according to MSUALG_6:def_1 ::_thesis: ( Args (o,A) <> {} implies Result (o,A) <> {} ) Result (o,B) <> {} ; hence ( Args (o,A) <> {} implies Result (o,A) <> {} ) ; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; cluster non-empty for MSAlgebra over S; existence ex b1 being MSAlgebra over S st b1 is non-empty proof set A = the non-empty MSAlgebra over S; take the non-empty MSAlgebra over S ; ::_thesis: the non-empty MSAlgebra over S is non-empty thus the non-empty MSAlgebra over S is non-empty ; ::_thesis: verum end; end; definition let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; mode Endomorphism of A -> ManySortedFunction of A,A means :Def2: :: MSUALG_6:def 2 it is_homomorphism A,A; existence ex b1 being ManySortedFunction of A,A st b1 is_homomorphism A,A proof take id the Sorts of A ; ::_thesis: id the Sorts of A is_homomorphism A,A thus id the Sorts of A is_homomorphism A,A by MSUALG_3:9; ::_thesis: verum end; end; :: deftheorem Def2 defines Endomorphism MSUALG_6:def_2_:_ for S being non empty non void ManySortedSign for A being MSAlgebra over S for b3 being ManySortedFunction of A,A holds ( b3 is Endomorphism of A iff b3 is_homomorphism A,A ); theorem Th4: :: MSUALG_6:4 for S being non empty non void ManySortedSign for A being MSAlgebra over S holds id the Sorts of A is Endomorphism of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S holds id the Sorts of A is Endomorphism of A let A be MSAlgebra over S; ::_thesis: id the Sorts of A is Endomorphism of A thus id the Sorts of A is_homomorphism A,A by MSUALG_3:9; :: according to MSUALG_6:def_2 ::_thesis: verum end; theorem Th5: :: MSUALG_6:5 for S being non empty non void ManySortedSign for A being MSAlgebra over S for h1, h2 being ManySortedFunction of A,A for o being OperSymbol of S for a being Element of Args (o,A) st a in Args (o,A) holds h2 # (h1 # a) = (h2 ** h1) # a proof let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S for h1, h2 being ManySortedFunction of A,A for o being OperSymbol of S for a being Element of Args (o,A) st a in Args (o,A) holds h2 # (h1 # a) = (h2 ** h1) # a let A be MSAlgebra over S; ::_thesis: for h1, h2 being ManySortedFunction of A,A for o being OperSymbol of S for a being Element of Args (o,A) st a in Args (o,A) holds h2 # (h1 # a) = (h2 ** h1) # a let h1, h2 be ManySortedFunction of A,A; ::_thesis: for o being OperSymbol of S for a being Element of Args (o,A) st a in Args (o,A) holds h2 # (h1 # a) = (h2 ** h1) # a set h = h2 ** h1; let o be OperSymbol of S; ::_thesis: for a being Element of Args (o,A) st a in Args (o,A) holds h2 # (h1 # a) = (h2 ** h1) # a let a be Element of Args (o,A); ::_thesis: ( a in Args (o,A) implies h2 # (h1 # a) = (h2 ** h1) # a ) assume A1: a in Args (o,A) ; ::_thesis: h2 # (h1 # a) = (h2 ** h1) # a then reconsider f = a, b = h1 # a, c = h2 # (h1 # a) as Function by Th1; A2: dom f = dom (the_arity_of o) by A1, Th2; now__::_thesis:_for_i_being_Nat_st_i_in_dom_f_holds_ c_._i_=_((h2_**_h1)_._((the_arity_of_o)_/._i))_._(f_._i) A3: dom ( the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3; A4: Args (o,A) = product ( the Sorts of A * (the_arity_of o)) by PRALG_2:3; let i be Nat; ::_thesis: ( i in dom f implies c . i = ((h2 ** h1) . ((the_arity_of o) /. i)) . (f . i) ) reconsider f1 = h1 . ((the_arity_of o) /. i), f2 = h2 . ((the_arity_of o) /. i) as Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . ((the_arity_of o) /. i)) ; A5: (h2 ** h1) . ((the_arity_of o) /. i) = f2 * f1 by MSUALG_3:2; assume A6: i in dom f ; ::_thesis: c . i = ((h2 ** h1) . ((the_arity_of o) /. i)) . (f . i) then A7: f1 . (f . i) = b . i by A1, MSUALG_3:24; dom b = dom (the_arity_of o) by A1, Th2; then A8: f2 . (b . i) = c . i by A1, A2, A6, MSUALG_3:24; A9: the Sorts of A . ((the_arity_of o) . i) = ( the Sorts of A * (the_arity_of o)) . i by A2, A6, FUNCT_1:13; (the_arity_of o) /. i = (the_arity_of o) . i by A2, A6, PARTFUN1:def_6; then f . i in the Sorts of A . ((the_arity_of o) /. i) by A1, A2, A6, A4, A3, A9, CARD_3:9; hence c . i = ((h2 ** h1) . ((the_arity_of o) /. i)) . (f . i) by A5, A7, A8, FUNCT_2:15; ::_thesis: verum end; hence h2 # (h1 # a) = (h2 ** h1) # a by A1, MSUALG_3:24; ::_thesis: verum end; theorem Th6: :: MSUALG_6:6 for S being non empty non void ManySortedSign for A being MSAlgebra over S for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A let A be MSAlgebra over S; ::_thesis: for h1, h2 being Endomorphism of A holds h2 ** h1 is Endomorphism of A let h1, h2 be Endomorphism of A; ::_thesis: h2 ** h1 is Endomorphism of A let o be OperSymbol of S; :: according to MSUALG_3:def_7,MSUALG_6:def_2 ::_thesis: ( Args (o,A) = {} or for b1 being Element of Args (o,A) holds ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,A)) . ((h2 ** h1) # b1) ) assume A1: Args (o,A) <> {} ; ::_thesis: for b1 being Element of Args (o,A) holds ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,A)) . ((h2 ** h1) # b1) set h = h2 ** h1; let x be Element of Args (o,A); ::_thesis: ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,A)) . ((h2 ** h1) # x) A2: Result (o,A) = the Sorts of A . (the_result_sort_of o) by PRALG_2:3; A3: h2 is_homomorphism A,A by Def2; reconsider f1 = h1 . (the_result_sort_of o), f2 = h2 . (the_result_sort_of o), f = (h2 ** h1) . (the_result_sort_of o) as Function of ( the Sorts of A . (the_result_sort_of o)),( the Sorts of A . (the_result_sort_of o)) ; A4: h1 is_homomorphism A,A by Def2; percases ( the Sorts of A . (the_result_sort_of o) = {} or the Sorts of A . (the_result_sort_of o) <> {} ) ; supposeA5: the Sorts of A . (the_result_sort_of o) = {} ; ::_thesis: ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,A)) . ((h2 ** h1) # x) then dom f = {} ; then A6: f . ((Den (o,A)) . x) = {} by FUNCT_1:def_2; dom (Den (o,A)) = {} by A2, A5; hence ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,A)) . ((h2 ** h1) # x) by A6, FUNCT_1:def_2; ::_thesis: verum end; supposeA7: the Sorts of A . (the_result_sort_of o) <> {} ; ::_thesis: ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,A)) . ((h2 ** h1) # x) (h2 ** h1) . (the_result_sort_of o) = f2 * f1 by MSUALG_3:2; then ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = f2 . (f1 . ((Den (o,A)) . x)) by A1, A2, A7, FUNCT_2:5, FUNCT_2:15 .= (h2 . (the_result_sort_of o)) . ((Den (o,A)) . (h1 # x)) by A4, A1, MSUALG_3:def_7 .= (Den (o,A)) . (h2 # (h1 # x)) by A3, A1, MSUALG_3:def_7 ; hence ((h2 ** h1) . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,A)) . ((h2 ** h1) # x) by A1, Th5; ::_thesis: verum end; end; end; definition let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; let h1, h2 be Endomorphism of A; :: original: ** redefine funch2 ** h1 -> Endomorphism of A; coherence h2 ** h1 is Endomorphism of A by Th6; end; definition let S be non empty non void ManySortedSign ; func TranslationRel S -> Relation of the carrier of S means :Def3: :: MSUALG_6:def 3 for s1, s2 being SortSymbol of S holds ( [s1,s2] in it iff ex o being OperSymbol of S st ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ); existence ex b1 being Relation of the carrier of S st for s1, s2 being SortSymbol of S holds ( [s1,s2] in b1 iff ex o being OperSymbol of S st ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) proof defpred S1[ set , set ] means ex o being OperSymbol of S st ( the_result_sort_of o = \$2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = \$1 ) ); ex R being Relation of the carrier of S, the carrier of S st for x, y being SortSymbol of S holds ( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2(); hence ex b1 being Relation of the carrier of S st for s1, s2 being SortSymbol of S holds ( [s1,s2] in b1 iff ex o being OperSymbol of S st ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) ; ::_thesis: verum end; correctness uniqueness for b1, b2 being Relation of the carrier of S st ( for s1, s2 being SortSymbol of S holds ( [s1,s2] in b1 iff ex o being OperSymbol of S st ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) ) & ( for s1, s2 being SortSymbol of S holds ( [s1,s2] in b2 iff ex o being OperSymbol of S st ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) ) holds b1 = b2; proof defpred S1[ set , set ] means ex o being OperSymbol of S st ( the_result_sort_of o = \$2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = \$1 ) ); for R1, R2 being Relation of the carrier of S, the carrier of S st ( for x, y being SortSymbol of S holds ( [x,y] in R1 iff S1[x,y] ) ) & ( for x, y being SortSymbol of S holds ( [x,y] in R2 iff S1[x,y] ) ) holds R1 = R2 from PUA2MSS1:sch_2(); hence for b1, b2 being Relation of the carrier of S st ( for s1, s2 being SortSymbol of S holds ( [s1,s2] in b1 iff ex o being OperSymbol of S st ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) ) & ( for s1, s2 being SortSymbol of S holds ( [s1,s2] in b2 iff ex o being OperSymbol of S st ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def3 defines TranslationRel MSUALG_6:def_3_:_ for S being non empty non void ManySortedSign for b2 being Relation of the carrier of S holds ( b2 = TranslationRel S iff for s1, s2 being SortSymbol of S holds ( [s1,s2] in b2 iff ex o being OperSymbol of S st ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) ); theorem Th7: :: MSUALG_6:7 for S being non empty non void ManySortedSign for o being OperSymbol of S for A being MSAlgebra over S for a being Function st a in Args (o,A) holds for i being Element of NAT for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A) proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for A being MSAlgebra over S for a being Function st a in Args (o,A) holds for i being Element of NAT for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A) let o be OperSymbol of S; ::_thesis: for A being MSAlgebra over S for a being Function st a in Args (o,A) holds for i being Element of NAT for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A) let A be MSAlgebra over S; ::_thesis: for a being Function st a in Args (o,A) holds for i being Element of NAT for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A) A1: dom ( the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3; let a be Function; ::_thesis: ( a in Args (o,A) implies for i being Element of NAT for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A) ) assume A2: a in Args (o,A) ; ::_thesis: for i being Element of NAT for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A) A3: dom a = dom (the_arity_of o) by A2, Th2; let i be Element of NAT ; ::_thesis: for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A) let x be Element of A,((the_arity_of o) /. i); ::_thesis: a +* (i,x) in Args (o,A) A4: Args (o,A) = product ( the Sorts of A * (the_arity_of o)) by PRALG_2:3; A5: now__::_thesis:_for_j_being_set_st_j_in_dom_a_holds_ (a_+*_(i,x))_._j_in_(_the_Sorts_of_A_*_(the_arity_of_o))_._j let j be set ; ::_thesis: ( j in dom a implies (a +* (i,x)) . b1 in ( the Sorts of A * (the_arity_of o)) . b1 ) assume A6: j in dom a ; ::_thesis: (a +* (i,x)) . b1 in ( the Sorts of A * (the_arity_of o)) . b1 then reconsider k = j as Element of NAT by A3; A7: ( the Sorts of A * (the_arity_of o)) . k = the Sorts of A . ((the_arity_of o) . k) by A3, A6, FUNCT_1:13; A8: (the_arity_of o) /. k = (the_arity_of o) . k by A3, A6, PARTFUN1:def_6; then A9: ( the Sorts of A * (the_arity_of o)) . j <> {} by A2, A3, A6, A7, Th3; percases ( j = i or j <> i ) ; supposeA10: j = i ; ::_thesis: (a +* (i,x)) . b1 in ( the Sorts of A * (the_arity_of o)) . b1 then (a +* (i,x)) . j = x by A6, FUNCT_7:31; hence (a +* (i,x)) . j in ( the Sorts of A * (the_arity_of o)) . j by A8, A7, A9, A10; ::_thesis: verum end; suppose j <> i ; ::_thesis: (a +* (i,x)) . b1 in ( the Sorts of A * (the_arity_of o)) . b1 then (a +* (i,x)) . j = a . j by FUNCT_7:32; hence (a +* (i,x)) . j in ( the Sorts of A * (the_arity_of o)) . j by A2, A4, A1, A3, A6, CARD_3:9; ::_thesis: verum end; end; end; dom (a +* (i,x)) = dom a by FUNCT_7:30; hence a +* (i,x) in Args (o,A) by A4, A1, A3, A5, CARD_3:9; ::_thesis: verum end; theorem Th8: :: MSUALG_6:8 for S being non empty non void ManySortedSign for A1, A2 being MSAlgebra over S for h being ManySortedFunction of A1,A2 for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds for i being Element of NAT st i in dom (the_arity_of o) holds for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) proof let S be non empty non void ManySortedSign ; ::_thesis: for A1, A2 being MSAlgebra over S for h being ManySortedFunction of A1,A2 for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds for i being Element of NAT st i in dom (the_arity_of o) holds for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) let A1, A2 be MSAlgebra over S; ::_thesis: for h being ManySortedFunction of A1,A2 for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds for i being Element of NAT st i in dom (the_arity_of o) holds for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) let h be ManySortedFunction of A1,A2; ::_thesis: for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds for i being Element of NAT st i in dom (the_arity_of o) holds for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) let o be OperSymbol of S; ::_thesis: ( Args (o,A1) <> {} & Args (o,A2) <> {} implies for i being Element of NAT st i in dom (the_arity_of o) holds for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) ) assume that A1: Args (o,A1) <> {} and A2: Args (o,A2) <> {} ; ::_thesis: for i being Element of NAT st i in dom (the_arity_of o) holds for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) let i be Element of NAT ; ::_thesis: ( i in dom (the_arity_of o) implies for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) ) assume A3: i in dom (the_arity_of o) ; ::_thesis: for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) then A4: the Sorts of A2 . ((the_arity_of o) /. i) <> {} by A2, Th3; the Sorts of A1 . ((the_arity_of o) /. i) <> {} by A1, A3, Th3; hence for x being Element of A1,((the_arity_of o) /. i) holds (h . ((the_arity_of o) /. i)) . x in the Sorts of A2 . ((the_arity_of o) /. i) by A4, FUNCT_2:5; ::_thesis: verum end; theorem Th9: :: MSUALG_6:9 for S being non empty non void ManySortedSign for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for A1, A2 being MSAlgebra over S for h being ManySortedFunction of A1,A2 for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for A1, A2 being MSAlgebra over S for h being ManySortedFunction of A1,A2 for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) let o be OperSymbol of S; ::_thesis: for i being Element of NAT st i in dom (the_arity_of o) holds for A1, A2 being MSAlgebra over S for h being ManySortedFunction of A1,A2 for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) let i be Element of NAT ; ::_thesis: ( i in dom (the_arity_of o) implies for A1, A2 being MSAlgebra over S for h being ManySortedFunction of A1,A2 for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) ) assume A1: i in dom (the_arity_of o) ; ::_thesis: for A1, A2 being MSAlgebra over S for h being ManySortedFunction of A1,A2 for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) let A1, A2 be MSAlgebra over S; ::_thesis: for h being ManySortedFunction of A1,A2 for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) let h be ManySortedFunction of A1,A2; ::_thesis: for a, b being Element of Args (o,A1) st a in Args (o,A1) & h # a in Args (o,A2) holds for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) let a, b be Element of Args (o,A1); ::_thesis: ( a in Args (o,A1) & h # a in Args (o,A2) implies for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) ) assume that A2: a in Args (o,A1) and A3: h # a in Args (o,A2) ; ::_thesis: for f, g1, g2 being Function st f = a & g1 = h # a & g2 = h # b holds for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) reconsider f2 = b as Function by A2, Th1; A4: dom f2 = dom (the_arity_of o) by A2, Th2; let f, g1, g2 be Function; ::_thesis: ( f = a & g1 = h # a & g2 = h # b implies for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) ) assume that A5: f = a and A6: g1 = h # a and A7: g2 = h # b ; ::_thesis: for x being Element of A1,((the_arity_of o) /. i) st b = f +* (i,x) holds ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) reconsider g3 = g1 +* (i,(g2 . i)) as Function ; A8: dom f = dom (the_arity_of o) by A2, A5, Th2; let x be Element of A1,((the_arity_of o) /. i); ::_thesis: ( b = f +* (i,x) implies ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) ) assume A9: b = f +* (i,x) ; ::_thesis: ( g2 . i = (h . ((the_arity_of o) /. i)) . x & h # b = g1 +* (i,(g2 . i)) ) f2 . i = x by A1, A9, A8, FUNCT_7:31; hence g2 . i = (h . ((the_arity_of o) /. i)) . x by A1, A2, A3, A7, A4, MSUALG_3:24; ::_thesis: h # b = g1 +* (i,(g2 . i)) then g2 . i in the Sorts of A2 . ((the_arity_of o) /. i) by A1, A2, A3, Th8; then g1 +* (i,(g2 . i)) in Args (o,A2) by A3, A6, Th7; then A10: dom g3 = dom (the_arity_of o) by Th2; A11: now__::_thesis:_for_z_being_set_st_z_in_dom_(the_arity_of_o)_&_z_<>_i_holds_ g2_._z_=_g1_._z let z be set ; ::_thesis: ( z in dom (the_arity_of o) & z <> i implies g2 . z = g1 . z ) assume that A12: z in dom (the_arity_of o) and A13: z <> i ; ::_thesis: g2 . z = g1 . z reconsider j = z as Element of NAT by A12; A14: f2 . j = f . j by A9, A13, FUNCT_7:32; g2 . j = (h . ((the_arity_of o) /. j)) . (f2 . j) by A2, A3, A7, A4, A12, MSUALG_3:24; hence g2 . z = g1 . z by A2, A3, A5, A6, A8, A12, A14, MSUALG_3:24; ::_thesis: verum end; A15: dom g1 = dom (the_arity_of o) by A3, A6, Th2; A16: now__::_thesis:_for_z_being_set_st_z_in_dom_(the_arity_of_o)_holds_ g2_._z_=_(g1_+*_(i,(g2_._i)))_._z let z be set ; ::_thesis: ( z in dom (the_arity_of o) implies g2 . b1 = (g1 +* (i,(g2 . i))) . b1 ) assume A17: z in dom (the_arity_of o) ; ::_thesis: g2 . b1 = (g1 +* (i,(g2 . i))) . b1 percases ( z = i or z <> i ) ; suppose z = i ; ::_thesis: g2 . b1 = (g1 +* (i,(g2 . i))) . b1 hence g2 . z = (g1 +* (i,(g2 . i))) . z by A1, A15, FUNCT_7:31; ::_thesis: verum end; supposeA18: z <> i ; ::_thesis: g2 . b1 = (g1 +* (i,(g2 . i))) . b1 then g2 . z = g1 . z by A11, A17; hence g2 . z = (g1 +* (i,(g2 . i))) . z by A18, FUNCT_7:32; ::_thesis: verum end; end; end; dom g2 = dom (the_arity_of o) by A3, A7, Th2; hence h # b = g1 +* (i,(g2 . i)) by A7, A10, A16, FUNCT_1:2; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let o be OperSymbol of S; let i be Element of NAT ; let A be MSAlgebra over S; let a be Function; func transl (o,i,a,A) -> Function means :Def4: :: MSUALG_6:def 4 ( dom it = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds it . x = (Den (o,A)) . (a +* (i,x)) ) ); existence ex b1 being Function st ( dom b1 = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds b1 . x = (Den (o,A)) . (a +* (i,x)) ) ) proof deffunc H1( set ) -> set = (Den (o,A)) . (a +* (i,\$1)); ex f being Function st ( dom f = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds b1 . x = (Den (o,A)) . (a +* (i,x)) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds b1 . x = (Den (o,A)) . (a +* (i,x)) ) & dom b2 = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds b2 . x = (Den (o,A)) . (a +* (i,x)) ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds f1 . x = (Den (o,A)) . (a +* (i,x)) ) & dom f2 = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds f2 . x = (Den (o,A)) . (a +* (i,x)) ) implies f1 = f2 ) assume that A1: dom f1 = the Sorts of A . ((the_arity_of o) /. i) and A2: for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds f1 . x = (Den (o,A)) . (a +* (i,x)) and A3: dom f2 = the Sorts of A . ((the_arity_of o) /. i) and A4: for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds f2 . x = (Den (o,A)) . (a +* (i,x)) ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in_the_Sorts_of_A_._((the_arity_of_o)_/._i)_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in the Sorts of A . ((the_arity_of o) /. i) implies f1 . x = f2 . x ) assume A5: x in the Sorts of A . ((the_arity_of o) /. i) ; ::_thesis: f1 . x = f2 . x then f1 . x = (Den (o,A)) . (a +* (i,x)) by A2; hence f1 . x = f2 . x by A4, A5; ::_thesis: verum end; hence f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines transl MSUALG_6:def_4_:_ for S being non empty non void ManySortedSign for o being OperSymbol of S for i being Element of NAT for A being MSAlgebra over S for a, b6 being Function holds ( b6 = transl (o,i,a,A) iff ( dom b6 = the Sorts of A . ((the_arity_of o) /. i) & ( for x being set st x in the Sorts of A . ((the_arity_of o) /. i) holds b6 . x = (Den (o,A)) . (a +* (i,x)) ) ) ); theorem Th10: :: MSUALG_6:10 for S being non empty non void ManySortedSign for o being OperSymbol of S for i being Element of NAT for A being feasible MSAlgebra over S for a being Function st a in Args (o,A) holds transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o)) proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for i being Element of NAT for A being feasible MSAlgebra over S for a being Function st a in Args (o,A) holds transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o)) let o be OperSymbol of S; ::_thesis: for i being Element of NAT for A being feasible MSAlgebra over S for a being Function st a in Args (o,A) holds transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o)) let i be Element of NAT ; ::_thesis: for A being feasible MSAlgebra over S for a being Function st a in Args (o,A) holds transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o)) let A be feasible MSAlgebra over S; ::_thesis: for a being Function st a in Args (o,A) holds transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o)) let a be Function; ::_thesis: ( a in Args (o,A) implies transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o)) ) assume A1: a in Args (o,A) ; ::_thesis: transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o)) then A2: Result (o,A) <> {} by Def1; A3: dom (transl (o,i,a,A)) = the Sorts of A . ((the_arity_of o) /. i) by Def4; A4: rng (transl (o,i,a,A)) c= the Sorts of A . (the_result_sort_of o) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (transl (o,i,a,A)) or x in the Sorts of A . (the_result_sort_of o) ) assume x in rng (transl (o,i,a,A)) ; ::_thesis: x in the Sorts of A . (the_result_sort_of o) then consider y being set such that A5: y in dom (transl (o,i,a,A)) and A6: x = (transl (o,i,a,A)) . y by FUNCT_1:def_3; reconsider y = y as Element of A,((the_arity_of o) /. i) by A5, Def4; set b = a +* (i,y); A7: (Den (o,A)) . (a +* (i,y)) in Result (o,A) by A1, A2, Th7, FUNCT_2:5; x = (Den (o,A)) . (a +* (i,y)) by A3, A5, A6, Def4; hence x in the Sorts of A . (the_result_sort_of o) by A7, PRALG_2:3; ::_thesis: verum end; Result (o,A) = the Sorts of A . (the_result_sort_of o) by PRALG_2:3; hence transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o)) by A2, A3, A4, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let s1, s2 be SortSymbol of S; let A be MSAlgebra over S; let f be Function; predf is_e.translation_of A,s1,s2 means :Def5: :: MSUALG_6:def 5 ex o being OperSymbol of S st ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st ( a in Args (o,A) & f = transl (o,i,a,A) ) ) ); end; :: deftheorem Def5 defines is_e.translation_of MSUALG_6:def_5_:_ for S being non empty non void ManySortedSign for s1, s2 being SortSymbol of S for A being MSAlgebra over S for f being Function holds ( f is_e.translation_of A,s1,s2 iff ex o being OperSymbol of S st ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st ( a in Args (o,A) & f = transl (o,i,a,A) ) ) ) ); theorem Th11: :: MSUALG_6:11 for S being non empty non void ManySortedSign for s1, s2 being SortSymbol of S for A being feasible MSAlgebra over S for f being Function st f is_e.translation_of A,s1,s2 holds ( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) proof let S be non empty non void ManySortedSign ; ::_thesis: for s1, s2 being SortSymbol of S for A being feasible MSAlgebra over S for f being Function st f is_e.translation_of A,s1,s2 holds ( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) let s1, s2 be SortSymbol of S; ::_thesis: for A being feasible MSAlgebra over S for f being Function st f is_e.translation_of A,s1,s2 holds ( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) let A be feasible MSAlgebra over S; ::_thesis: for f being Function st f is_e.translation_of A,s1,s2 holds ( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) let f be Function; ::_thesis: ( f is_e.translation_of A,s1,s2 implies ( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) assume f is_e.translation_of A,s1,s2 ; ::_thesis: ( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) then consider o being OperSymbol of S such that A1: the_result_sort_of o = s2 and A2: ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st ( a in Args (o,A) & f = transl (o,i,a,A) ) ) by Def5; Result (o,A) = the Sorts of A . (the_result_sort_of o) by PRALG_2:3; hence ( f is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) by A1, A2, Def1, Th3, Th10; ::_thesis: verum end; theorem Th12: :: MSUALG_6:12 for S being non empty non void ManySortedSign for s1, s2 being SortSymbol of S for A being MSAlgebra over S for f being Function st f is_e.translation_of A,s1,s2 holds [s1,s2] in TranslationRel S proof let S be non empty non void ManySortedSign ; ::_thesis: for s1, s2 being SortSymbol of S for A being MSAlgebra over S for f being Function st f is_e.translation_of A,s1,s2 holds [s1,s2] in TranslationRel S let s1, s2 be SortSymbol of S; ::_thesis: for A being MSAlgebra over S for f being Function st f is_e.translation_of A,s1,s2 holds [s1,s2] in TranslationRel S let A be MSAlgebra over S; ::_thesis: for f being Function st f is_e.translation_of A,s1,s2 holds [s1,s2] in TranslationRel S let f be Function; ::_thesis: ( f is_e.translation_of A,s1,s2 implies [s1,s2] in TranslationRel S ) assume f is_e.translation_of A,s1,s2 ; ::_thesis: [s1,s2] in TranslationRel S then ex o being OperSymbol of S st ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st ( a in Args (o,A) & f = transl (o,i,a,A) ) ) ) by Def5; hence [s1,s2] in TranslationRel S by Def3; ::_thesis: verum end; theorem :: MSUALG_6:13 for S being non empty non void ManySortedSign for s1, s2 being SortSymbol of S for A being non-empty MSAlgebra over S st [s1,s2] in TranslationRel S holds ex f being Function st f is_e.translation_of A,s1,s2 proof let S be non empty non void ManySortedSign ; ::_thesis: for s1, s2 being SortSymbol of S for A being non-empty MSAlgebra over S st [s1,s2] in TranslationRel S holds ex f being Function st f is_e.translation_of A,s1,s2 let s1, s2 be SortSymbol of S; ::_thesis: for A being non-empty MSAlgebra over S st [s1,s2] in TranslationRel S holds ex f being Function st f is_e.translation_of A,s1,s2 let A be non-empty MSAlgebra over S; ::_thesis: ( [s1,s2] in TranslationRel S implies ex f being Function st f is_e.translation_of A,s1,s2 ) assume [s1,s2] in TranslationRel S ; ::_thesis: ex f being Function st f is_e.translation_of A,s1,s2 then consider o being OperSymbol of S such that A1: the_result_sort_of o = s2 and A2: ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) by Def3; set a = the Element of Args (o,A); consider i being Element of NAT such that A3: i in dom (the_arity_of o) and A4: (the_arity_of o) /. i = s1 by A2; take transl (o,i, the Element of Args (o,A),A) ; ::_thesis: transl (o,i, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 take o ; :: according to MSUALG_6:def_5 ::_thesis: ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st ( a in Args (o,A) & transl (o,i, the Element of Args (o,A),A) = transl (o,i,a,A) ) ) ) thus ( the_result_sort_of o = s2 & ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st ( a in Args (o,A) & transl (o,i, the Element of Args (o,A),A) = transl (o,i,a,A) ) ) ) by A1, A3, A4; ::_thesis: verum end; theorem Th14: :: MSUALG_6:14 for S being non empty non void ManySortedSign for A being feasible MSAlgebra over S for s1, s2 being SortSymbol of S for q being RedSequence of TranslationRel S for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) holds ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being feasible MSAlgebra over S for s1, s2 being SortSymbol of S for q being RedSequence of TranslationRel S for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) holds ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) let A be feasible MSAlgebra over S; ::_thesis: for s1, s2 being SortSymbol of S for q being RedSequence of TranslationRel S for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) holds ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) let s1, s2 be SortSymbol of S; ::_thesis: for q being RedSequence of TranslationRel S for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) holds ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) let q be RedSequence of TranslationRel S; ::_thesis: for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) holds ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) let p be Function-yielding FinSequence; ::_thesis: ( len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) implies ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) ) assume that A1: len q = (len p) + 1 and A2: s1 = q . 1 and A3: s2 = q . (len q) and A4: for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ; ::_thesis: ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) percases ( p = {} or p <> {} ) ; supposeA5: p = {} ; ::_thesis: ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) then A6: len p = 0 ; compose (p,( the Sorts of A . s1)) = id ( the Sorts of A . s1) by A5, FUNCT_7:39; hence ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) by A1, A2, A3, A6; ::_thesis: verum end; suppose p <> {} ; ::_thesis: ( compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) & ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) ) then A7: rng p <> {} ; then A8: 1 in dom p by FINSEQ_3:32; then A9: 1 + 1 in dom q by A1, FUNCT_7:22; 1 in dom q by A1, A8, FUNCT_7:22; then [(q . 1),(q . (1 + 1))] in TranslationRel S by A9, REWRITE1:def_2; then reconsider q1 = q . 1, q2 = q . (1 + 1) as SortSymbol of S by ZFMISC_1:87; deffunc H1( set ) -> set = the Sorts of A . (q . \$1); reconsider f = p . 1 as Function ; A10: dom q = Seg (len q) by FINSEQ_1:def_3; consider pp being FinSequence such that A11: len pp = len q and A12: for i being Nat st i in dom pp holds pp . i = H1(i) from FINSEQ_1:sch_2(); defpred S1[ Element of NAT ] means ( \$1 in dom pp implies not pp . \$1 is empty ); A13: dom pp = Seg (len q) by A11, FINSEQ_1:def_3; f is_e.translation_of A,q1,q2 by A4, A7, FINSEQ_3:32; then A14: the Sorts of A . q1 <> {} by Th11; A15: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume that ( i in dom pp implies not pp . i is empty ) and A16: i + 1 in dom pp ; ::_thesis: not pp . (i + 1) is empty A17: i <= i + 1 by NAT_1:11; i + 1 <= len pp by A16, FINSEQ_3:25; then A18: i <= len pp by A17, XXREAL_0:2; percases ( i = 0 or i > 0 ) ; suppose i = 0 ; ::_thesis: not pp . (i + 1) is empty hence not pp . (i + 1) is empty by A14, A12, A16; ::_thesis: verum end; suppose i > 0 ; ::_thesis: not pp . (i + 1) is empty then i >= 0 + 1 by NAT_1:13; then A19: i in dom pp by A18, FINSEQ_3:25; then [(q . i),(q . (i + 1))] in TranslationRel S by A10, A13, A16, REWRITE1:def_2; then reconsider s1 = q . i, s2 = q . (i + 1) as SortSymbol of S by ZFMISC_1:87; reconsider f = p . i as Function ; i in dom p by A1, A11, A16, A19, FUNCT_7:22; then A20: f is_e.translation_of A,s1,s2 by A4; pp . (i + 1) = the Sorts of A . s2 by A12, A16; hence not pp . (i + 1) is empty by A20, Th11; ::_thesis: verum end; end; end; A21: S1[ 0 ] by FINSEQ_3:25; A22: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A21, A15); A23: pp is non-empty proof let x be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not x in proj1 pp or not pp . x is empty ) assume x in dom pp ; ::_thesis: not pp . x is empty hence not pp . x is empty by A22; ::_thesis: verum end; A24: dom pp = Seg (len q) by A11, FINSEQ_1:def_3; reconsider pp = pp as non empty non-empty FinSequence by A11, A23; A25: dom p = Seg (len p) by FINSEQ_1:def_3; p is FuncSequence of pp proof thus (len p) + 1 = len pp by A1, A11; :: according to FUNCT_7:def_10 ::_thesis: for b1 being Element of NAT holds ( not b1 in dom p or p . b1 in K97((pp . b1),(pp . (b1 + 1))) ) let j be Element of NAT ; ::_thesis: ( not j in dom p or p . j in K97((pp . j),(pp . (j + 1))) ) reconsider f = p . j as Function ; assume A26: j in dom p ; ::_thesis: p . j in K97((pp . j),(pp . (j + 1))) then A27: j >= 1 by A25, FINSEQ_1:1; then A28: j + 1 >= 1 by NAT_1:13; A29: j <= len p by A25, A26, FINSEQ_1:1; then j <= len q by A1, NAT_1:13; then A30: j in Seg (len q) by A27, FINSEQ_1:1; j + 1 <= len q by A1, A29, XREAL_1:6; then A31: j + 1 in Seg (len q) by A28, FINSEQ_1:1; then [(q . j),(q . (j + 1))] in TranslationRel S by A10, A30, REWRITE1:def_2; then reconsider s1 = q . j, s2 = q . (j + 1) as SortSymbol of S by ZFMISC_1:87; A32: pp . (j + 1) = the Sorts of A . s2 by A12, A24, A31; A33: f is_e.translation_of A,s1,s2 by A4, A26; then A34: p . j is Function of ( the Sorts of A . s1),( the Sorts of A . s2) by Th11; A35: the Sorts of A . s2 <> {} by A33, Th11; pp . j = the Sorts of A . s1 by A12, A24, A30; hence p . j in K97((pp . j),(pp . (j + 1))) by A34, A35, A32, FUNCT_2:8; ::_thesis: verum end; then reconsider p9 = p as FuncSequence of pp ; A36: 1 in dom q by FINSEQ_5:6; then A37: pp . 1 = the Sorts of A . s1 by A2, A10, A12, A13; then A38: dom (compose (p9,( the Sorts of A . s1))) = the Sorts of A . s1 by FUNCT_7:67; A39: len q in dom q by FINSEQ_5:6; then A40: pp . (len pp) = the Sorts of A . s2 by A3, A10, A11, A12, A13; then rng (compose (p9,( the Sorts of A . s1))) c= the Sorts of A . s2 by A37, FUNCT_7:67; hence compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) by A10, A11, A13, A39, A40, A38, FUNCT_2:def_1, RELSET_1:4; ::_thesis: ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) thus ( p <> {} implies ( the Sorts of A . s1 <> {} & the Sorts of A . s2 <> {} ) ) by A10, A11, A13, A36, A39, A37, A40; ::_thesis: verum end; end; end; definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let s1, s2 be SortSymbol of S; assume B1: TranslationRel S reduces s1,s2 ; mode Translation of A,s1,s2 -> Function of ( the Sorts of A . s1),( the Sorts of A . s2) means :Def6: :: MSUALG_6:def 6 ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st ( it = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ); existence ex b1 being Function of ( the Sorts of A . s1),( the Sorts of A . s2) ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st ( b1 = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) proof consider q being RedSequence of TranslationRel S such that A1: q . 1 = s1 and A2: q . (len q) = s2 by B1, REWRITE1:def_3; defpred S1[ set , set ] means ex f being Function ex s1, s2 being SortSymbol of S ex i being Element of NAT st ( \$2 = f & i = \$1 & s1 = q . i & s2 = q . (i + 1) & f is_e.translation_of A,s1,s2 ); len q >= 0 + 1 by NAT_1:13; then consider n being Nat such that A3: len q = 1 + n by NAT_1:10; reconsider n = n as Element of NAT by ORDINAL1:def_12; A4: dom q = Seg (len q) by FINSEQ_1:def_3; A5: for x being set st x in Seg n holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in Seg n implies ex y being set st S1[x,y] ) assume A6: x in Seg n ; ::_thesis: ex y being set st S1[x,y] then reconsider i = x as Element of NAT ; A7: i <= n by A6, FINSEQ_1:1; then A8: i + 1 <= len q by A3, XREAL_1:6; A9: i >= 1 by A6, FINSEQ_1:1; then i + 1 >= 1 by NAT_1:13; then A10: i + 1 in dom q by A4, A8, FINSEQ_1:1; i <= n + 1 by A7, NAT_1:13; then i in dom q by A3, A4, A9, FINSEQ_1:1; then A11: [(q . i),(q . (i + 1))] in TranslationRel S by A10, REWRITE1:def_2; then reconsider s1 = q . i, s2 = q . (i + 1) as SortSymbol of S by ZFMISC_1:87; consider o being OperSymbol of S such that A12: the_result_sort_of o = s2 and A13: ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) by A11, Def3; set a = the Element of Args (o,A); consider j being Element of NAT such that A14: j in dom (the_arity_of o) and A15: (the_arity_of o) /. j = s1 by A13; take transl (o,j, the Element of Args (o,A),A) ; ::_thesis: S1[x, transl (o,j, the Element of Args (o,A),A)] take transl (o,j, the Element of Args (o,A),A) ; ::_thesis: ex s1, s2 being SortSymbol of S ex i being Element of NAT st ( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 ) take s1 ; ::_thesis: ex s2 being SortSymbol of S ex i being Element of NAT st ( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 ) take s2 ; ::_thesis: ex i being Element of NAT st ( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 ) take i ; ::_thesis: ( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 ) thus ( transl (o,j, the Element of Args (o,A),A) = transl (o,j, the Element of Args (o,A),A) & i = x & s1 = q . i & s2 = q . (i + 1) & transl (o,j, the Element of Args (o,A),A) is_e.translation_of A,s1,s2 ) by A12, A14, A15, Def5; ::_thesis: verum end; consider p being Function such that A16: ( dom p = Seg n & ( for x being set st x in Seg n holds S1[x,p . x] ) ) from CLASSES1:sch_1(A5); p is Function-yielding proof let j be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not j in proj1 p or p . j is set ) assume j in dom p ; ::_thesis: p . j is set then ex f being Function ex s1, s2 being SortSymbol of S ex i being Element of NAT st ( p . j = f & i = j & s1 = q . i & s2 = q . (i + 1) & f is_e.translation_of A,s1,s2 ) by A16; hence p . j is set ; ::_thesis: verum end; then reconsider p = p as Function-yielding FinSequence by A16, FINSEQ_1:def_2; A17: now__::_thesis:_for_i_being_Element_of_NAT_ for_f_being_Function for_s1,_s2_being_SortSymbol_of_S_st_i_in_dom_p_&_f_=_p_._i_&_s1_=_q_._i_&_s2_=_q_._(i_+_1)_holds_ f_is_e.translation_of_A,s1,s2 let i be Element of NAT ; ::_thesis: for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 let f be Function; ::_thesis: for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 let s1, s2 be SortSymbol of S; ::_thesis: ( i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) implies f is_e.translation_of A,s1,s2 ) assume i in dom p ; ::_thesis: ( f = p . i & s1 = q . i & s2 = q . (i + 1) implies f is_e.translation_of A,s1,s2 ) then ex f being Function ex s1, s2 being SortSymbol of S ex j being Element of NAT st ( p . i = f & j = i & s1 = q . j & s2 = q . (j + 1) & f is_e.translation_of A,s1,s2 ) by A16; hence ( f = p . i & s1 = q . i & s2 = q . (i + 1) implies f is_e.translation_of A,s1,s2 ) ; ::_thesis: verum end; len p = n by A16, FINSEQ_1:def_3; then reconsider t = compose (p,( the Sorts of A . s1)) as Function of ( the Sorts of A . s1),( the Sorts of A . s2) by A1, A2, A3, A17, Th14; take t ; ::_thesis: ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st ( t = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) take q ; ::_thesis: ex p being Function-yielding FinSequence st ( t = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) take p ; ::_thesis: ( t = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) thus ( t = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) by A1, A2, A3, A16, A17, FINSEQ_1:def_3; ::_thesis: verum end; end; :: deftheorem Def6 defines Translation MSUALG_6:def_6_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for b5 being Function of ( the Sorts of A . s1),( the Sorts of A . s2) holds ( b5 is Translation of A,s1,s2 iff ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st ( b5 = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) ); theorem :: MSUALG_6:15 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for q being RedSequence of TranslationRel S for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) holds compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2 proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for q being RedSequence of TranslationRel S for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) holds compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2 let A be non-empty MSAlgebra over S; ::_thesis: for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for q being RedSequence of TranslationRel S for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) holds compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2 let s1, s2 be SortSymbol of S; ::_thesis: ( TranslationRel S reduces s1,s2 implies for q being RedSequence of TranslationRel S for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) holds compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2 ) assume A1: TranslationRel S reduces s1,s2 ; ::_thesis: for q being RedSequence of TranslationRel S for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) holds compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2 let q be RedSequence of TranslationRel S; ::_thesis: for p being Function-yielding FinSequence st len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) holds compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2 let p be Function-yielding FinSequence; ::_thesis: ( len q = (len p) + 1 & s1 = q . 1 & s2 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) implies compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2 ) assume that A2: len q = (len p) + 1 and A3: s1 = q . 1 and A4: s2 = q . (len q) and A5: for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ; ::_thesis: compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2 compose (p,( the Sorts of A . s1)) is Function of ( the Sorts of A . s1),( the Sorts of A . s2) by A2, A3, A4, A5, Th14; hence compose (p,( the Sorts of A . s1)) is Translation of A,s1,s2 by A1, A2, A3, A4, A5, Def6; ::_thesis: verum end; theorem Th16: :: MSUALG_6:16 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for s being SortSymbol of S holds id ( the Sorts of A . s) is Translation of A,s,s proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for s being SortSymbol of S holds id ( the Sorts of A . s) is Translation of A,s,s let A be non-empty MSAlgebra over S; ::_thesis: for s being SortSymbol of S holds id ( the Sorts of A . s) is Translation of A,s,s let s be SortSymbol of S; ::_thesis: id ( the Sorts of A . s) is Translation of A,s,s thus TranslationRel S reduces s,s by REWRITE1:12; :: according to MSUALG_6:def_6 ::_thesis: ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st ( id ( the Sorts of A . s) = compose (p,( the Sorts of A . s)) & len q = (len p) + 1 & s = q . 1 & s = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) A1: <*s*> is RedSequence of TranslationRel S by REWRITE1:6; A2: len <*s*> = 0 + 1 by FINSEQ_1:40; A3: len {} = 0 ; A4: for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom {} & f = {} . i & s1 = <*s*> . i & s2 = <*s*> . (i + 1) holds f is_e.translation_of A,s1,s2 ; A5: <*s*> . 1 = s by FINSEQ_1:40; id ( the Sorts of A . s) = compose ({},( the Sorts of A . s)) by FUNCT_7:39; hence ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st ( id ( the Sorts of A . s) = compose (p,( the Sorts of A . s)) & len q = (len p) + 1 & s = q . 1 & s = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) by A1, A2, A3, A5, A4; ::_thesis: verum end; theorem Th17: :: MSUALG_6:17 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for s1, s2 being SortSymbol of S for f being Function st f is_e.translation_of A,s1,s2 holds ( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for s1, s2 being SortSymbol of S for f being Function st f is_e.translation_of A,s1,s2 holds ( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 ) let A be non-empty MSAlgebra over S; ::_thesis: for s1, s2 being SortSymbol of S for f being Function st f is_e.translation_of A,s1,s2 holds ( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 ) let s1, s2 be SortSymbol of S; ::_thesis: for f being Function st f is_e.translation_of A,s1,s2 holds ( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 ) let f be Function; ::_thesis: ( f is_e.translation_of A,s1,s2 implies ( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 ) ) A1: len <*s1,s2*> = 1 + 1 by FINSEQ_1:44; A2: len <*f*> = 1 by FINSEQ_1:40; assume A3: f is_e.translation_of A,s1,s2 ; ::_thesis: ( TranslationRel S reduces s1,s2 & f is Translation of A,s1,s2 ) then reconsider g = f as Function of ( the Sorts of A . s1),( the Sorts of A . s2) by Th11; A4: <*s1,s2*> . 2 = s2 by FINSEQ_1:44; A5: <*s1,s2*> . 1 = s1 by FINSEQ_1:44; A6: now__::_thesis:_for_i_being_Element_of_NAT_ for_g_being_Function for_w1,_w2_being_SortSymbol_of_S_st_i_in_dom_<*f*>_&_g_=_<*f*>_._i_&_w1_=_<*s1,s2*>_._i_&_w2_=_<*s1,s2*>_._(i_+_1)_holds_ g_is_e.translation_of_A,w1,w2 let i be Element of NAT ; ::_thesis: for g being Function for w1, w2 being SortSymbol of S st i in dom <*f*> & g = <*f*> . i & w1 = <*s1,s2*> . i & w2 = <*s1,s2*> . (i + 1) holds g is_e.translation_of A,w1,w2 let g be Function; ::_thesis: for w1, w2 being SortSymbol of S st i in dom <*f*> & g = <*f*> . i & w1 = <*s1,s2*> . i & w2 = <*s1,s2*> . (i + 1) holds g is_e.translation_of A,w1,w2 let w1, w2 be SortSymbol of S; ::_thesis: ( i in dom <*f*> & g = <*f*> . i & w1 = <*s1,s2*> . i & w2 = <*s1,s2*> . (i + 1) implies g is_e.translation_of A,w1,w2 ) assume i in dom <*f*> ; ::_thesis: ( g = <*f*> . i & w1 = <*s1,s2*> . i & w2 = <*s1,s2*> . (i + 1) implies g is_e.translation_of A,w1,w2 ) then i in {1} by FINSEQ_1:2, FINSEQ_1:38; then i = 1 by TARSKI:def_1; hence ( g = <*f*> . i & w1 = <*s1,s2*> . i & w2 = <*s1,s2*> . (i + 1) implies g is_e.translation_of A,w1,w2 ) by A3, A5, A4, FINSEQ_1:40; ::_thesis: verum end; dom g = the Sorts of A . s1 by FUNCT_2:def_1; then A7: g = compose (<*f*>,( the Sorts of A . s1)) by FUNCT_7:46; A8: [s1,s2] in TranslationRel S by A3, Th12; hence A9: TranslationRel S reduces s1,s2 by REWRITE1:15; ::_thesis: f is Translation of A,s1,s2 <*s1,s2*> is RedSequence of TranslationRel S by A8, REWRITE1:7; hence f is Translation of A,s1,s2 by A7, A9, A1, A2, A5, A4, A6, Def6; ::_thesis: verum end; theorem Th18: :: MSUALG_6:18 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 & TranslationRel S reduces s2,s3 holds for t1 being Translation of A,s1,s2 for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3 proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 & TranslationRel S reduces s2,s3 holds for t1 being Translation of A,s1,s2 for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3 let A be non-empty MSAlgebra over S; ::_thesis: for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 & TranslationRel S reduces s2,s3 holds for t1 being Translation of A,s1,s2 for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3 let s1, s2, s3 be SortSymbol of S; ::_thesis: ( TranslationRel S reduces s1,s2 & TranslationRel S reduces s2,s3 implies for t1 being Translation of A,s1,s2 for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3 ) assume that A1: TranslationRel S reduces s1,s2 and A2: TranslationRel S reduces s2,s3 ; ::_thesis: for t1 being Translation of A,s1,s2 for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3 let t1 be Translation of A,s1,s2; ::_thesis: for t2 being Translation of A,s2,s3 holds t2 * t1 is Translation of A,s1,s3 let t2 be Translation of A,s2,s3; ::_thesis: t2 * t1 is Translation of A,s1,s3 thus TranslationRel S reduces s1,s3 by A1, A2, REWRITE1:16; :: according to MSUALG_6:def_6 ::_thesis: ex q being RedSequence of TranslationRel S ex p being Function-yielding FinSequence st ( t2 * t1 = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s3 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) consider q1 being RedSequence of TranslationRel S, p1 being Function-yielding FinSequence such that A3: t1 = compose (p1,( the Sorts of A . s1)) and A4: len q1 = (len p1) + 1 and A5: s1 = q1 . 1 and A6: s2 = q1 . (len q1) and A7: for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p1 & f = p1 . i & s1 = q1 . i & s2 = q1 . (i + 1) holds f is_e.translation_of A,s1,s2 by A1, Def6; consider q2 being RedSequence of TranslationRel S, p2 being Function-yielding FinSequence such that A8: t2 = compose (p2,( the Sorts of A . s2)) and A9: len q2 = (len p2) + 1 and A10: s2 = q2 . 1 and A11: s3 = q2 . (len q2) and A12: for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p2 & f = p2 . i & s1 = q2 . i & s2 = q2 . (i + 1) holds f is_e.translation_of A,s1,s2 by A2, Def6; reconsider q = q1 \$^ q2 as RedSequence of TranslationRel S by A6, A10, REWRITE1:8; take q ; ::_thesis: ex p being Function-yielding FinSequence st ( t2 * t1 = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s3 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) take p = p1 ^ p2; ::_thesis: ( t2 * t1 = compose (p,( the Sorts of A . s1)) & len q = (len p) + 1 & s1 = q . 1 & s3 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) rng t1 c= the Sorts of A . s2 by RELAT_1:def_19; hence t2 * t1 = compose (p,( the Sorts of A . s1)) by A3, A8, FUNCT_7:48; ::_thesis: ( len q = (len p) + 1 & s1 = q . 1 & s3 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) A13: len p = (len p1) + (len p2) by FINSEQ_1:22; consider x2 being set , r2 being FinSequence such that A14: q2 = <*x2*> ^ r2 and len q2 = (len r2) + 1 by REWRITE1:5; A15: x2 = s2 by A10, A14, FINSEQ_1:41; consider r1 being FinSequence, x1 being set such that A16: q1 = r1 ^ <*x1*> by FINSEQ_1:46; A17: q = r1 ^ q2 by A16, REWRITE1:2; len <*x1*> = 1 by FINSEQ_1:40; then A18: len q1 = (len r1) + 1 by A16, FINSEQ_1:22; then A19: len q = (len p1) + (len q2) by A4, A17, FINSEQ_1:22; hence len q = (len p) + 1 by A9, A13; ::_thesis: ( s1 = q . 1 & s3 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) x1 = s2 by A6, A16, A18, FINSEQ_1:42; then A20: q = q1 ^ r2 by A16, A14, A17, A15, FINSEQ_1:32; ( 1 <= len r1 or 0 + 1 > len r1 ) ; then A21: ( ( 1 in Seg (len r1) & Seg (len r1) = dom r1 ) or ( 0 <= len r1 & 0 >= len r1 ) ) by FINSEQ_1:1, FINSEQ_1:def_3, NAT_1:13; then A22: ( ( q . 1 = r1 . 1 & r1 . 1 = q1 . 1 ) or ( r1 = {} & {} ^ q2 = q2 ) ) by A16, A17, FINSEQ_1:34, FINSEQ_1:def_7; ( ( q . 1 = r1 . 1 & r1 . 1 = q1 . 1 ) or ( len r1 = 0 & {} ^ q2 = q2 ) ) by A16, A17, A21, FINSEQ_1:34, FINSEQ_1:def_7; hence s1 = q . 1 by A5, A6, A10, A16, A18, A22, REWRITE1:2; ::_thesis: ( s3 = q . (len q) & ( for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 ) ) len q2 in dom q2 by FINSEQ_5:6; hence s3 = q . (len q) by A4, A11, A18, A17, A19, FINSEQ_1:def_7; ::_thesis: for i being Element of NAT for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 let i be Element of NAT ; ::_thesis: for f being Function for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 let f be Function; ::_thesis: for s1, s2 being SortSymbol of S st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of A,s1,s2 let s1, s2 be SortSymbol of S; ::_thesis: ( i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) implies f is_e.translation_of A,s1,s2 ) assume that A23: i in dom p and A24: f = p . i and A25: s1 = q . i and A26: s2 = q . (i + 1) ; ::_thesis: f is_e.translation_of A,s1,s2 percases ( i in dom p1 or not i in dom p1 ) ; supposeA27: i in dom p1 ; ::_thesis: f is_e.translation_of A,s1,s2 then i + 1 in dom q1 by A4, FUNCT_7:22; then A28: s2 = q1 . (i + 1) by A20, A26, FINSEQ_1:def_7; i in dom q1 by A4, A27, FUNCT_7:22; then A29: s1 = q1 . i by A20, A25, FINSEQ_1:def_7; f = p1 . i by A24, A27, FINSEQ_1:def_7; hence f is_e.translation_of A,s1,s2 by A7, A27, A29, A28; ::_thesis: verum end; suppose not i in dom p1 ; ::_thesis: f is_e.translation_of A,s1,s2 then ( not i <= len p1 or not i >= 1 ) by FINSEQ_3:25; then i >= (len p1) + 1 by A23, FINSEQ_3:25, NAT_1:13; then consider k being Nat such that A30: i = ((len p1) + 1) + k by NAT_1:10; A31: (len p1) + ((k + 1) + 1) = i + 1 by A30; A32: k + 1 >= 1 by NAT_1:11; A33: i = (len p1) + (1 + k) by A30; i <= len p by A23, FINSEQ_3:25; then k + 1 <= len p2 by A13, A33, XREAL_1:6; then A34: k + 1 in dom p2 by A32, FINSEQ_3:25; then k + 1 in dom q2 by A9, FUNCT_7:22; then A35: s1 = q2 . (k + 1) by A4, A18, A17, A25, A33, FINSEQ_1:def_7; (k + 1) + 1 in dom q2 by A9, A34, FUNCT_7:22; then A36: s2 = q2 . ((k + 1) + 1) by A4, A18, A17, A26, A31, FINSEQ_1:def_7; f = p2 . (k + 1) by A24, A33, A34, FINSEQ_1:def_7; hence f is_e.translation_of A,s1,s2 by A12, A34, A35, A36; ::_thesis: verum end; end; end; theorem Th19: :: MSUALG_6:19 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A,s1,s2 for f being Function st f is_e.translation_of A,s2,s3 holds f * t is Translation of A,s1,s3 proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A,s1,s2 for f being Function st f is_e.translation_of A,s2,s3 holds f * t is Translation of A,s1,s3 let A be non-empty MSAlgebra over S; ::_thesis: for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A,s1,s2 for f being Function st f is_e.translation_of A,s2,s3 holds f * t is Translation of A,s1,s3 let s1, s2, s3 be SortSymbol of S; ::_thesis: ( TranslationRel S reduces s1,s2 implies for t being Translation of A,s1,s2 for f being Function st f is_e.translation_of A,s2,s3 holds f * t is Translation of A,s1,s3 ) assume A1: TranslationRel S reduces s1,s2 ; ::_thesis: for t being Translation of A,s1,s2 for f being Function st f is_e.translation_of A,s2,s3 holds f * t is Translation of A,s1,s3 let t be Translation of A,s1,s2; ::_thesis: for f being Function st f is_e.translation_of A,s2,s3 holds f * t is Translation of A,s1,s3 let f be Function; ::_thesis: ( f is_e.translation_of A,s2,s3 implies f * t is Translation of A,s1,s3 ) assume A2: f is_e.translation_of A,s2,s3 ; ::_thesis: f * t is Translation of A,s1,s3 then A3: f is Translation of A,s2,s3 by Th17; TranslationRel S reduces s2,s3 by A2, Th17; hence f * t is Translation of A,s1,s3 by A1, A3, Th18; ::_thesis: verum end; theorem :: MSUALG_6:20 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s2,s3 holds for f being Function st f is_e.translation_of A,s1,s2 holds for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3 proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s2,s3 holds for f being Function st f is_e.translation_of A,s1,s2 holds for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3 let A be non-empty MSAlgebra over S; ::_thesis: for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s2,s3 holds for f being Function st f is_e.translation_of A,s1,s2 holds for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3 let s1, s2, s3 be SortSymbol of S; ::_thesis: ( TranslationRel S reduces s2,s3 implies for f being Function st f is_e.translation_of A,s1,s2 holds for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3 ) assume A1: TranslationRel S reduces s2,s3 ; ::_thesis: for f being Function st f is_e.translation_of A,s1,s2 holds for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3 let f be Function; ::_thesis: ( f is_e.translation_of A,s1,s2 implies for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3 ) assume A2: f is_e.translation_of A,s1,s2 ; ::_thesis: for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3 then A3: f is Translation of A,s1,s2 by Th17; TranslationRel S reduces s1,s2 by A2, Th17; hence for t being Translation of A,s2,s3 holds t * f is Translation of A,s1,s3 by A1, A3, Th18; ::_thesis: verum end; scheme :: MSUALG_6:sch 1 TranslationInd{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), P1[ set , set , set ] } : for s1, s2 being SortSymbol of F1() st TranslationRel F1() reduces s1,s2 holds for t being Translation of F2(),s1,s2 holds P1[t,s1,s2] provided A1: for s being SortSymbol of F1() holds P1[ id ( the Sorts of F2() . s),s,s] and A2: for s1, s2, s3 being SortSymbol of F1() st TranslationRel F1() reduces s1,s2 holds for t being Translation of F2(),s1,s2 st P1[t,s1,s2] holds for f being Function st f is_e.translation_of F2(),s2,s3 holds P1[f * t,s1,s3] proof set S = F1(); set A = F2(); let s1, s2 be SortSymbol of F1(); ::_thesis: ( TranslationRel F1() reduces s1,s2 implies for t being Translation of F2(),s1,s2 holds P1[t,s1,s2] ) assume A3: TranslationRel F1() reduces s1,s2 ; ::_thesis: for t being Translation of F2(),s1,s2 holds P1[t,s1,s2] let t be Translation of F2(),s1,s2; ::_thesis: P1[t,s1,s2] consider q being RedSequence of TranslationRel F1(), p being Function-yielding FinSequence such that A4: t = compose (p,( the Sorts of F2() . s1)) and A5: len q = (len p) + 1 and A6: s1 = q . 1 and A7: s2 = q . (len q) and A8: for i being Element of NAT for f being Function for s1, s2 being SortSymbol of F1() st i in dom p & f = p . i & s1 = q . i & s2 = q . (i + 1) holds f is_e.translation_of F2(),s1,s2 by A3, Def6; defpred S1[ Element of NAT ] means ( \$1 in dom p implies ex s being SortSymbol of F1() ex t being Translation of F2(),s1,s ex p9 being Function-yielding FinSequence st ( p9 = p | (Seg \$1) & s = q . (\$1 + 1) & TranslationRel F1() reduces s1,s & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,s] ) ); A9: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume that A10: ( i in dom p implies ex s being SortSymbol of F1() ex t being Translation of F2(),s1,s ex p9 being Function-yielding FinSequence st ( p9 = p | (Seg i) & s = q . (i + 1) & TranslationRel F1() reduces s1,s & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,s] ) ) and A11: i + 1 in dom p ; ::_thesis: ex s being SortSymbol of F1() ex t being Translation of F2(),s1,s ex p9 being Function-yielding FinSequence st ( p9 = p | (Seg (i + 1)) & s = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,s & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,s] ) A12: (i + 1) + 1 in dom q by A5, A11, FUNCT_7:22; i + 1 in dom q by A5, A11, FUNCT_7:22; then [(q . (i + 1)),(q . ((i + 1) + 1))] in TranslationRel F1() by A12, REWRITE1:def_2; then reconsider v1 = q . (i + 1), v2 = q . ((i + 1) + 1) as SortSymbol of F1() by ZFMISC_1:87; reconsider f = p . (i + 1) as Function ; A13: f is_e.translation_of F2(),v1,v2 by A8, A11; then reconsider t = f as Translation of F2(),v1,v2 by Th17; percases ( i = 0 or i > 0 ) ; supposeA14: i = 0 ; ::_thesis: ex s being SortSymbol of F1() ex t being Translation of F2(),s1,s ex p9 being Function-yielding FinSequence st ( p9 = p | (Seg (i + 1)) & s = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,s & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,s] ) then reconsider t = t as Translation of F2(),s1,v2 by A6; reconsider p9 = p | (Seg 1) as Function-yielding FinSequence by FINSEQ_1:15; A15: t * (id ( the Sorts of F2() . s1)) = t by FUNCT_2:17; take v2 ; ::_thesis: ex t being Translation of F2(),s1,v2 ex p9 being Function-yielding FinSequence st ( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] ) take t ; ::_thesis: ex p9 being Function-yielding FinSequence st ( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] ) take p9 ; ::_thesis: ( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] ) thus ( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) ) by A14; ::_thesis: ( TranslationRel F1() reduces s1,v2 & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] ) thus TranslationRel F1() reduces s1,v2 by A6, A13, A14, Th17; ::_thesis: ( t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] ) A16: dom t = the Sorts of F2() . s1 by FUNCT_2:def_1; 1 in Seg 1 by FINSEQ_1:2, TARSKI:def_1; then A17: p9 . 1 = t by A14, FUNCT_1:49; 0 + 1 <= len p by A11, A14, FINSEQ_3:25; then len p9 = 1 by FINSEQ_1:17; then p9 = <*t*> by A17, FINSEQ_1:40; hence t = compose (p9,( the Sorts of F2() . s1)) by A16, FUNCT_7:46; ::_thesis: P1[t,s1,v2] A18: TranslationRel F1() reduces s1,s1 by REWRITE1:12; A19: P1[ id ( the Sorts of F2() . s1),s1,s1] by A1; id ( the Sorts of F2() . s1) is Translation of F2(),s1,s1 by Th16; hence P1[t,s1,v2] by A2, A6, A8, A11, A14, A18, A15, A19; ::_thesis: verum end; supposeA20: i > 0 ; ::_thesis: ex s being SortSymbol of F1() ex t being Translation of F2(),s1,s ex p9 being Function-yielding FinSequence st ( p9 = p | (Seg (i + 1)) & s = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,s & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,s] ) reconsider pp = p | (Seg (i + 1)) as FinSequence by FINSEQ_1:15; take v2 ; ::_thesis: ex t being Translation of F2(),s1,v2 ex p9 being Function-yielding FinSequence st ( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,v2] ) A21: i + 1 <= len p by A11, FINSEQ_3:25; then A22: i <= len p by NAT_1:13; i >= 0 + 1 by A20, NAT_1:13; then consider s being SortSymbol of F1(), t9 being Translation of F2(),s1,s, p9 being Function-yielding FinSequence such that A23: p9 = p | (Seg i) and A24: s = q . (i + 1) and A25: TranslationRel F1() reduces s1,s and A26: t9 = compose (p9,( the Sorts of F2() . s1)) and A27: P1[t9,s1,s] by A10, A22, FINSEQ_3:25; reconsider T = t * t9 as Translation of F2(),s1,v2 by A8, A11, A24, A25, Th19; take T ; ::_thesis: ex p9 being Function-yielding FinSequence st ( p9 = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & T = compose (p9,( the Sorts of F2() . s1)) & P1[T,s1,v2] ) take y = p9 ^ <*f*>; ::_thesis: ( y = p | (Seg (i + 1)) & v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & T = compose (y,( the Sorts of F2() . s1)) & P1[T,s1,v2] ) i <= len p by A21, NAT_1:13; then A28: len p9 = i by A23, FINSEQ_1:17; i + 1 <= len p by A11, FINSEQ_3:25; then A29: dom pp = Seg (i + 1) by FINSEQ_1:17; A30: now__::_thesis:_for_k_being_Nat_st_k_in_Seg_(i_+_1)_holds_ y_._k_=_pp_._k let k be Nat; ::_thesis: ( k in Seg (i + 1) implies y . k = pp . k ) assume A31: k in Seg (i + 1) ; ::_thesis: y . k = pp . k then k <= i + 1 by FINSEQ_1:1; then ( ( k <= i & k >= 1 ) or k = i + 1 ) by A31, FINSEQ_1:1, NAT_1:8; then ( k in dom p9 or k = i + 1 ) by A28, FINSEQ_3:25; then ( ( y . k = p9 . k & p9 . k = p . k ) or y . k = p . k ) by A23, A28, FINSEQ_1:42, FINSEQ_1:def_7, FUNCT_1:47; hence y . k = pp . k by A29, A31, FUNCT_1:47; ::_thesis: verum end; len <*f*> = 1 by FINSEQ_1:40; then len y = (len p9) + 1 by FINSEQ_1:22; then dom y = Seg (i + 1) by A28, FINSEQ_1:def_3; hence y = p | (Seg (i + 1)) by A29, A30, FINSEQ_1:13; ::_thesis: ( v2 = q . ((i + 1) + 1) & TranslationRel F1() reduces s1,v2 & T = compose (y,( the Sorts of F2() . s1)) & P1[T,s1,v2] ) thus v2 = q . ((i + 1) + 1) ; ::_thesis: ( TranslationRel F1() reduces s1,v2 & T = compose (y,( the Sorts of F2() . s1)) & P1[T,s1,v2] ) TranslationRel F1() reduces v1,v2 by A13, Th17; hence TranslationRel F1() reduces s1,v2 by A24, A25, REWRITE1:16; ::_thesis: ( T = compose (y,( the Sorts of F2() . s1)) & P1[T,s1,v2] ) thus T = compose (y,( the Sorts of F2() . s1)) by A26, FUNCT_7:41; ::_thesis: P1[T,s1,v2] thus P1[T,s1,v2] by A2, A8, A11, A24, A25, A27; ::_thesis: verum end; end; end; A32: S1[ 0 ] by FINSEQ_3:25; A33: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A32, A9); percases ( p = {} or p <> {} ) ; supposeA34: p = {} ; ::_thesis: P1[t,s1,s2] then A35: len p = 0 ; t = id ( the Sorts of F2() . s1) by A4, A34, FUNCT_7:39; hence P1[t,s1,s2] by A1, A5, A6, A7, A35; ::_thesis: verum end; suppose p <> {} ; ::_thesis: P1[t,s1,s2] then len p >= 0 + 1 by NAT_1:13; then A36: len p in dom p by FINSEQ_3:25; A37: p | (dom p) = p ; dom p = Seg (len p) by FINSEQ_1:def_3; then ex s being SortSymbol of F1() ex t being Translation of F2(),s1,s ex p9 being Function-yielding FinSequence st ( p9 = p & s = q . ((len p) + 1) & TranslationRel F1() reduces s1,s & t = compose (p9,( the Sorts of F2() . s1)) & P1[t,s1,s] ) by A33, A36, A37; hence P1[t,s1,s2] by A4, A5, A7; ::_thesis: verum end; end; end; theorem Th21: :: MSUALG_6:21 for S being non empty non void ManySortedSign for A1, A2 being non-empty MSAlgebra over S for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for a being Element of Args (o,A1) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i)) proof let S be non empty non void ManySortedSign ; ::_thesis: for A1, A2 being non-empty MSAlgebra over S for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for a being Element of Args (o,A1) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i)) let A1, A2 be non-empty MSAlgebra over S; ::_thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for a being Element of Args (o,A1) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i)) let h be ManySortedFunction of A1,A2; ::_thesis: ( h is_homomorphism A1,A2 implies for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for a being Element of Args (o,A1) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i)) ) assume A1: h is_homomorphism A1,A2 ; ::_thesis: for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for a being Element of Args (o,A1) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i)) let o be OperSymbol of S; ::_thesis: for i being Element of NAT st i in dom (the_arity_of o) holds for a being Element of Args (o,A1) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i)) let i be Element of NAT ; ::_thesis: ( i in dom (the_arity_of o) implies for a being Element of Args (o,A1) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i)) ) assume A2: i in dom (the_arity_of o) ; ::_thesis: for a being Element of Args (o,A1) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i)) let a be Element of Args (o,A1); ::_thesis: (h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i)) set s1 = (the_arity_of o) /. i; set s2 = the_result_sort_of o; reconsider T = transl (o,i,(h # a),A2) as Function of ( the Sorts of A2 . ((the_arity_of o) /. i)),( the Sorts of A2 . (the_result_sort_of o)) by Th10; reconsider t = transl (o,i,a,A1) as Function of ( the Sorts of A1 . ((the_arity_of o) /. i)),( the Sorts of A1 . (the_result_sort_of o)) by Th10; now__::_thesis:_for_x_being_Element_of_A1,((the_arity_of_o)_/._i)_holds_((h_._(the_result_sort_of_o))_*_t)_._x_=_(T_*_(h_._((the_arity_of_o)_/._i)))_._x let x be Element of A1,((the_arity_of o) /. i); ::_thesis: ((h . (the_result_sort_of o)) * t) . x = (T * (h . ((the_arity_of o) /. i))) . x reconsider b = a +* (i,x) as Element of Args (o,A1) by Th7; A3: h # b = (h # a) +* (i,((h # b) . i)) by A2, Th9; h # a in Args (o,A2) ; then A4: (h # b) . i = (h . ((the_arity_of o) /. i)) . x by A2, Th9; thus ((h . (the_result_sort_of o)) * t) . x = (h . (the_result_sort_of o)) . (t . x) by FUNCT_2:15 .= (h . (the_result_sort_of o)) . ((Den (o,A1)) . b) by Def4 .= (Den (o,A2)) . ((h # a) +* (i,((h . ((the_arity_of o) /. i)) . x))) by A1, A4, A3, MSUALG_3:def_7 .= T . ((h . ((the_arity_of o) /. i)) . x) by Def4 .= (T * (h . ((the_arity_of o) /. i))) . x by FUNCT_2:15 ; ::_thesis: verum end; hence (h . (the_result_sort_of o)) * (transl (o,i,a,A1)) = (transl (o,i,(h # a),A2)) * (h . ((the_arity_of o) /. i)) by FUNCT_2:63; ::_thesis: verum end; theorem :: MSUALG_6:22 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for h being Endomorphism of A for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for a being Element of Args (o,A) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A)) = (transl (o,i,(h # a),A)) * (h . ((the_arity_of o) /. i)) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for h being Endomorphism of A for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for a being Element of Args (o,A) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A)) = (transl (o,i,(h # a),A)) * (h . ((the_arity_of o) /. i)) let A be non-empty MSAlgebra over S; ::_thesis: for h being Endomorphism of A for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for a being Element of Args (o,A) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A)) = (transl (o,i,(h # a),A)) * (h . ((the_arity_of o) /. i)) let h be Endomorphism of A; ::_thesis: for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for a being Element of Args (o,A) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A)) = (transl (o,i,(h # a),A)) * (h . ((the_arity_of o) /. i)) h is_homomorphism A,A by Def2; hence for o being OperSymbol of S for i being Element of NAT st i in dom (the_arity_of o) holds for a being Element of Args (o,A) holds (h . (the_result_sort_of o)) * (transl (o,i,a,A)) = (transl (o,i,(h # a),A)) * (h . ((the_arity_of o) /. i)) by Th21; ::_thesis: verum end; theorem Th23: :: MSUALG_6:23 for S being non empty non void ManySortedSign for A1, A2 being non-empty MSAlgebra over S for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A1,s1,s2 holds ex T being Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) st ( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A1, A2 being non-empty MSAlgebra over S for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A1,s1,s2 holds ex T being Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) st ( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t ) let A1, A2 be non-empty MSAlgebra over S; ::_thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A1,s1,s2 holds ex T being Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) st ( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t ) let h be ManySortedFunction of A1,A2; ::_thesis: ( h is_homomorphism A1,A2 implies for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A1,s1,s2 holds ex T being Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) st ( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t ) ) assume A1: h is_homomorphism A1,A2 ; ::_thesis: for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A1,s1,s2 holds ex T being Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) st ( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t ) let s1, s2 be SortSymbol of S; ::_thesis: for t being Function st t is_e.translation_of A1,s1,s2 holds ex T being Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) st ( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t ) let t be Function; ::_thesis: ( t is_e.translation_of A1,s1,s2 implies ex T being Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) st ( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t ) ) assume t is_e.translation_of A1,s1,s2 ; ::_thesis: ex T being Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) st ( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t ) then consider o being OperSymbol of S such that A2: the_result_sort_of o = s2 and A3: ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st ( a in Args (o,A1) & t = transl (o,i,a,A1) ) ) by Def5; consider i being Element of NAT , a being Function such that A4: i in dom (the_arity_of o) and A5: (the_arity_of o) /. i = s1 and A6: a in Args (o,A1) and A7: t = transl (o,i,a,A1) by A3; reconsider a = a as Element of Args (o,A1) by A6; reconsider T = transl (o,i,(h # a),A2) as Function of ( the Sorts of A2 . s1),( the Sorts of A2 . s2) by A2, A5, Th10; take T ; ::_thesis: ( T is_e.translation_of A2,s1,s2 & T * (h . s1) = (h . s2) * t ) thus T is_e.translation_of A2,s1,s2 by A2, A4, A5, Def5; ::_thesis: T * (h . s1) = (h . s2) * t thus T * (h . s1) = (h . s2) * t by A1, A2, A4, A5, A7, Th21; ::_thesis: verum end; theorem :: MSUALG_6:24 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for h being Endomorphism of A for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A,s1,s2 holds ex T being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st ( T is_e.translation_of A,s1,s2 & T * (h . s1) = (h . s2) * t ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for h being Endomorphism of A for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A,s1,s2 holds ex T being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st ( T is_e.translation_of A,s1,s2 & T * (h . s1) = (h . s2) * t ) let A be non-empty MSAlgebra over S; ::_thesis: for h being Endomorphism of A for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A,s1,s2 holds ex T being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st ( T is_e.translation_of A,s1,s2 & T * (h . s1) = (h . s2) * t ) let h be Endomorphism of A; ::_thesis: for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A,s1,s2 holds ex T being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st ( T is_e.translation_of A,s1,s2 & T * (h . s1) = (h . s2) * t ) h is_homomorphism A,A by Def2; hence for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A,s1,s2 holds ex T being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st ( T is_e.translation_of A,s1,s2 & T * (h . s1) = (h . s2) * t ) by Th23; ::_thesis: verum end; theorem Th25: :: MSUALG_6:25 for S being non empty non void ManySortedSign for A1, A2 being non-empty MSAlgebra over S for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t proof let S be non empty non void ManySortedSign ; ::_thesis: for A1, A2 being non-empty MSAlgebra over S for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t let A1, A2 be non-empty MSAlgebra over S; ::_thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t let h be ManySortedFunction of A1,A2; ::_thesis: ( h is_homomorphism A1,A2 implies for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t ) assume A1: h is_homomorphism A1,A2 ; ::_thesis: for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A1,s1,s2 ex T being Translation of A2,s1,s2 st T * (h . s1) = (h . s2) * t defpred S1[ Function, SortSymbol of S, SortSymbol of S] means ex T being Translation of A2,\$2,\$3 st T * (h . \$2) = (h . \$3) * \$1; A2: for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A1,s1,s2 st S1[t,s1,s2] holds for f being Function st f is_e.translation_of A1,s2,s3 holds S1[f * t,s1,s3] proof let s1, s2, s3 be SortSymbol of S; ::_thesis: ( TranslationRel S reduces s1,s2 implies for t being Translation of A1,s1,s2 st S1[t,s1,s2] holds for f being Function st f is_e.translation_of A1,s2,s3 holds S1[f * t,s1,s3] ) assume A3: TranslationRel S reduces s1,s2 ; ::_thesis: for t being Translation of A1,s1,s2 st S1[t,s1,s2] holds for f being Function st f is_e.translation_of A1,s2,s3 holds S1[f * t,s1,s3] let t be Translation of A1,s1,s2; ::_thesis: ( S1[t,s1,s2] implies for f being Function st f is_e.translation_of A1,s2,s3 holds S1[f * t,s1,s3] ) given T being Translation of A2,s1,s2 such that A4: T * (h . s1) = (h . s2) * t ; ::_thesis: for f being Function st f is_e.translation_of A1,s2,s3 holds S1[f * t,s1,s3] let f be Function; ::_thesis: ( f is_e.translation_of A1,s2,s3 implies S1[f * t,s1,s3] ) assume f is_e.translation_of A1,s2,s3 ; ::_thesis: S1[f * t,s1,s3] then consider T1 being Function of ( the Sorts of A2 . s2),( the Sorts of A2 . s3) such that A5: T1 is_e.translation_of A2,s2,s3 and A6: T1 * (h . s2) = (h . s3) * f by A1, Th23; reconsider T2 = T1 * T as Translation of A2,s1,s3 by A3, A5, Th19; take T2 ; ::_thesis: T2 * (h . s1) = (h . s3) * (f * t) thus T2 * (h . s1) = T1 * (T * (h . s1)) by RELAT_1:36 .= ((h . s3) * f) * t by A4, A6, RELAT_1:36 .= (h . s3) * (f * t) by RELAT_1:36 ; ::_thesis: verum end; A7: for s being SortSymbol of S holds S1[ id ( the Sorts of A1 . s),s,s] proof let s be SortSymbol of S; ::_thesis: S1[ id ( the Sorts of A1 . s),s,s] A8: (id ( the Sorts of A2 . s)) * (h . s) = h . s by FUNCT_2:17; A9: (h . s) * (id ( the Sorts of A1 . s)) = h . s by FUNCT_2:17; id ( the Sorts of A2 . s) is Translation of A2,s,s by Th16; hence S1[ id ( the Sorts of A1 . s),s,s] by A8, A9; ::_thesis: verum end; thus for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A1,s1,s2 holds S1[t,s1,s2] from MSUALG_6:sch_1(A7, A2); ::_thesis: verum end; theorem Th26: :: MSUALG_6:26 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for h being Endomorphism of A for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A,s1,s2 ex T being Translation of A,s1,s2 st T * (h . s1) = (h . s2) * t proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for h being Endomorphism of A for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A,s1,s2 ex T being Translation of A,s1,s2 st T * (h . s1) = (h . s2) * t let A be non-empty MSAlgebra over S; ::_thesis: for h being Endomorphism of A for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A,s1,s2 ex T being Translation of A,s1,s2 st T * (h . s1) = (h . s2) * t let h be Endomorphism of A; ::_thesis: for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A,s1,s2 ex T being Translation of A,s1,s2 st T * (h . s1) = (h . s2) * t h is_homomorphism A,A by Def2; hence for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A,s1,s2 ex T being Translation of A,s1,s2 st T * (h . s1) = (h . s2) * t by Th25; ::_thesis: verum end; begin definition let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; let R be ManySortedRelation of A; attrR is compatible means :Def7: :: MSUALG_6:def 7 for o being OperSymbol of S for a, b being Function st a in Args (o,A) & b in Args (o,A) & ( for n being Element of NAT st n in dom (the_arity_of o) holds [(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o); attrR is invariant means :Def8: :: MSUALG_6:def 8 for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A,s1,s2 holds for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2; attrR is stable means :Def9: :: MSUALG_6:def 9 for h being Endomorphism of A for s being SortSymbol of S for a, b being set st [a,b] in R . s holds [((h . s) . a),((h . s) . b)] in R . s; end; :: deftheorem Def7 defines compatible MSUALG_6:def_7_:_ for S being non empty non void ManySortedSign for A being MSAlgebra over S for R being ManySortedRelation of A holds ( R is compatible iff for o being OperSymbol of S for a, b being Function st a in Args (o,A) & b in Args (o,A) & ( for n being Element of NAT st n in dom (the_arity_of o) holds [(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) ); :: deftheorem Def8 defines invariant MSUALG_6:def_8_:_ for S being non empty non void ManySortedSign for A being MSAlgebra over S for R being ManySortedRelation of A holds ( R is invariant iff for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A,s1,s2 holds for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2 ); :: deftheorem Def9 defines stable MSUALG_6:def_9_:_ for S being non empty non void ManySortedSign for A being MSAlgebra over S for R being ManySortedRelation of A holds ( R is stable iff for h being Endomorphism of A for s being SortSymbol of S for a, b being set st [a,b] in R . s holds [((h . s) . a),((h . s) . b)] in R . s ); theorem :: MSUALG_6:27 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being MSEquivalence-like ManySortedRelation of A holds ( R is compatible iff R 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 MSEquivalence-like ManySortedRelation of A holds ( R is compatible iff R is MSCongruence of A ) let A be non-empty MSAlgebra over S; ::_thesis: for R being MSEquivalence-like ManySortedRelation of A holds ( R is compatible iff R is MSCongruence of A ) let R be MSEquivalence-like ManySortedRelation of A; ::_thesis: ( R is compatible iff R is MSCongruence of A ) hereby ::_thesis: ( R is MSCongruence of A implies R is compatible ) assume A1: R is compatible ; ::_thesis: R is MSCongruence of A now__::_thesis:_for_o_being_OperSymbol_of_S for_x,_y_being_Element_of_Args_(o,A)_st_(_for_n_being_Nat_st_n_in_dom_x_holds_ [(x_._n),(y_._n)]_in_R_._((the_arity_of_o)_/._n)_)_holds_ [((Den_(o,A))_._x),((Den_(o,A))_._y)]_in_R_._(the_result_sort_of_o) let o be OperSymbol of S; ::_thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds [(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . x),((Den (o,A)) . y)] in R . (the_result_sort_of o) let x, y be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom x holds [(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in R . (the_result_sort_of o) ) assume A2: for n being Nat st n in dom x holds [(x . n),(y . n)] in R . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in R . (the_result_sort_of o) now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(the_arity_of_o)_holds_ [(x_._n),(y_._n)]_in_R_._((the_arity_of_o)_/._n) let n be Element of NAT ; ::_thesis: ( n in dom (the_arity_of o) implies [(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) assume n in dom (the_arity_of o) ; ::_thesis: [(x . n),(y . n)] in R . ((the_arity_of o) /. n) then n in dom x by MSUALG_3:6; hence [(x . n),(y . n)] in R . ((the_arity_of o) /. n) by A2; ::_thesis: verum end; hence [((Den (o,A)) . x),((Den (o,A)) . y)] in R . (the_result_sort_of o) by A1, Def7; ::_thesis: verum end; hence R is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum end; assume A3: R is MSCongruence of A ; ::_thesis: R is compatible let o be OperSymbol of S; :: according to MSUALG_6:def_7 ::_thesis: for a, b being Function st a in Args (o,A) & b in Args (o,A) & ( for n being Element of NAT st n in dom (the_arity_of o) holds [(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) let x, y be Function; ::_thesis: ( x in Args (o,A) & y in Args (o,A) & ( for n being Element of NAT st n in dom (the_arity_of o) holds [(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in R . (the_result_sort_of o) ) assume that A4: x in Args (o,A) and A5: y in Args (o,A) and A6: for n being Element of NAT st n in dom (the_arity_of o) holds [(x . n),(y . n)] in R . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in R . (the_result_sort_of o) reconsider x = x, y = y as Element of Args (o,A) by A4, A5; now__::_thesis:_for_n_being_Nat_st_n_in_dom_x_holds_ [(x_._n),(y_._n)]_in_R_._((the_arity_of_o)_/._n) let n be Nat; ::_thesis: ( n in dom x implies [(x . n),(y . n)] in R . ((the_arity_of o) /. n) ) assume n in dom x ; ::_thesis: [(x . n),(y . n)] in R . ((the_arity_of o) /. n) then n in dom (the_arity_of o) by MSUALG_3:6; hence [(x . n),(y . n)] in R . ((the_arity_of o) /. n) by A6; ::_thesis: verum end; hence [((Den (o,A)) . x),((Den (o,A)) . y)] in R . (the_result_sort_of o) by A3, MSUALG_4:def_4; ::_thesis: verum end; theorem Th28: :: MSUALG_6:28 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of A holds ( R is invariant iff for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for f being Translation of A,s1,s2 for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being ManySortedRelation of A holds ( R is invariant iff for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for f being Translation of A,s1,s2 for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) let A be non-empty MSAlgebra over S; ::_thesis: for R being ManySortedRelation of A holds ( R is invariant iff for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for f being Translation of A,s1,s2 for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) let R be ManySortedRelation of A; ::_thesis: ( R is invariant iff for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for f being Translation of A,s1,s2 for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) hereby ::_thesis: ( ( for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for f being Translation of A,s1,s2 for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) implies R is invariant ) defpred S1[ Function, set , set ] means for a, b being set st [a,b] in R . \$2 holds [(\$1 . a),(\$1 . b)] in R . \$3; deffunc H1( SortSymbol of S) -> Element of bool [:( the Sorts of A . \$1),( the Sorts of A . \$1):] = id ( the Sorts of A . \$1); assume A1: R is invariant ; ::_thesis: for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A,s1,s2 holds S1[t,s1,s2] A2: for s1, s2, s3 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A,s1,s2 st S1[t,s1,s2] holds for f being Function st f is_e.translation_of A,s2,s3 holds S1[f * t,s1,s3] proof let s1, s2, s3 be SortSymbol of S; ::_thesis: ( TranslationRel S reduces s1,s2 implies for t being Translation of A,s1,s2 st S1[t,s1,s2] holds for f being Function st f is_e.translation_of A,s2,s3 holds S1[f * t,s1,s3] ) assume TranslationRel S reduces s1,s2 ; ::_thesis: for t being Translation of A,s1,s2 st S1[t,s1,s2] holds for f being Function st f is_e.translation_of A,s2,s3 holds S1[f * t,s1,s3] let t be Translation of A,s1,s2; ::_thesis: ( S1[t,s1,s2] implies for f being Function st f is_e.translation_of A,s2,s3 holds S1[f * t,s1,s3] ) assume A3: for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2 ; ::_thesis: for f being Function st f is_e.translation_of A,s2,s3 holds S1[f * t,s1,s3] let f be Function; ::_thesis: ( f is_e.translation_of A,s2,s3 implies S1[f * t,s1,s3] ) assume A4: f is_e.translation_of A,s2,s3 ; ::_thesis: S1[f * t,s1,s3] let a, b be set ; ::_thesis: ( [a,b] in R . s1 implies [((f * t) . a),((f * t) . b)] in R . s3 ) assume A5: [a,b] in R . s1 ; ::_thesis: [((f * t) . a),((f * t) . b)] in R . s3 then reconsider a9 = a, b9 = b as Element of A,s1 by ZFMISC_1:87; [(t . a9),(t . b9)] in R . s2 by A3, A5; then A6: [(f . (t . a9)),(f . (t . b9))] in R . s3 by A1, A4, Def8; f . (t . a9) = (f * t) . a9 by FUNCT_2:15; hence [((f * t) . a),((f * t) . b)] in R . s3 by A6, FUNCT_2:15; ::_thesis: verum end; A7: for s being SortSymbol of S holds S1[ id ( the Sorts of A . s),s,s] proof let s be SortSymbol of S; ::_thesis: S1[ id ( the Sorts of A . s),s,s] let a, b be set ; ::_thesis: ( [a,b] in R . s implies [((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)] in R . s ) assume A8: [a,b] in R . s ; ::_thesis: [((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)] in R . s then a in the Sorts of A . s by ZFMISC_1:87; then A9: H1(s) . a = a by FUNCT_1:17; b in the Sorts of A . s by A8, ZFMISC_1:87; hence [((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)] in R . s by A8, A9, FUNCT_1:17; ::_thesis: verum end; thus for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for t being Translation of A,s1,s2 holds S1[t,s1,s2] from MSUALG_6:sch_1(A7, A2); ::_thesis: verum end; assume A10: for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for f being Translation of A,s1,s2 for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ; ::_thesis: R is invariant let s1, s2 be SortSymbol of S; :: according to MSUALG_6:def_8 ::_thesis: for t being Function st t is_e.translation_of A,s1,s2 holds for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2 let t be Function; ::_thesis: ( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2 ) assume A11: t is_e.translation_of A,s1,s2 ; ::_thesis: for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2 then t is Translation of A,s1,s2 by Th17; hence for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2 by A10, A11, Th17; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; cluster MSEquivalence-like invariant -> MSEquivalence-like compatible for ManySortedRelation of the Sorts of A, the Sorts of A; coherence for b1 being MSEquivalence-like ManySortedRelation of A st b1 is invariant holds b1 is compatible proof let R be MSEquivalence-like ManySortedRelation of A; ::_thesis: ( R is invariant implies R is compatible ) assume A1: for s1, s2 being SortSymbol of S for t being Function st t is_e.translation_of A,s1,s2 holds for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2 ; :: according to MSUALG_6:def_8 ::_thesis: R is compatible let o be OperSymbol of S; :: according to MSUALG_6:def_7 ::_thesis: for a, b being Function st a in Args (o,A) & b in Args (o,A) & ( for n being Element of NAT st n in dom (the_arity_of o) holds [(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) let a, b be Function; ::_thesis: ( a in Args (o,A) & b in Args (o,A) & ( for n being Element of NAT st n in dom (the_arity_of o) holds [(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) ) assume that A2: a in Args (o,A) and A3: b in Args (o,A) and A4: for n being Element of NAT st n in dom (the_arity_of o) holds [(a . n),(b . n)] in R . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) A5: dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def_3; reconsider a9 = a as Element of Args (o,A) by A2; defpred S1[ set , set , set ] means ex c being Element of Args (o,A) st ( c = A & c3 = c +* (S,(b . S)) ); A6: for n being Element of NAT st 1 <= n & n < (len (the_arity_of o)) + 1 holds for x being Element of Args (o,A) ex y being Element of Args (o,A) st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n < (len (the_arity_of o)) + 1 implies for x being Element of Args (o,A) ex y being Element of Args (o,A) st S1[n,x,y] ) assume that A7: 1 <= n and A8: n < (len (the_arity_of o)) + 1 ; ::_thesis: for x being Element of Args (o,A) ex y being Element of Args (o,A) st S1[n,x,y] let x be Element of Args (o,A); ::_thesis: ex y being Element of Args (o,A) st S1[n,x,y] n <= len (the_arity_of o) by A8, NAT_1:13; then n in dom (the_arity_of o) by A7, FINSEQ_3:25; then b . n in the Sorts of A . ((the_arity_of o) /. n) by A3, Th2; then x +* (n,(b . n)) in Args (o,A) by Th7; hence ex y being Element of Args (o,A) st S1[n,x,y] ; ::_thesis: verum end; consider p being FinSequence of Args (o,A) such that A9: len p = (len (the_arity_of o)) + 1 and A10: ( p . 1 = a9 or (len (the_arity_of o)) + 1 = 0 ) and A11: for i being Element of NAT st 1 <= i & i < (len (the_arity_of o)) + 1 holds S1[i,p . i,p . (i + 1)] from RECDEF_1:sch_4(A6); (len (the_arity_of o)) + 1 >= 1 by NAT_1:11; then A12: (len (the_arity_of o)) + 1 in dom p by A9, FINSEQ_3:25; defpred S2[ Element of NAT ] means ( S <= len (the_arity_of o) implies ex c being Element of Args (o,A) st ( c = p . (S + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > S holds c . j = a . j ) & ( for j being Nat st j in Seg S holds c . j = b . j ) ) ); A13: dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def_3; A14: for n being Element of NAT st S2[n] holds S2[n + 1] proof let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] ) assume that A15: ( i <= len (the_arity_of o) implies ex c being Element of Args (o,A) st ( c = p . (i + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > i holds c . j = a . j ) & ( for j being Nat st j in Seg i holds c . j = b . j ) ) ) and A16: i + 1 <= len (the_arity_of o) ; ::_thesis: ex c being Element of Args (o,A) st ( c = p . ((i + 1) + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > i + 1 holds c . j = a . j ) & ( for j being Nat st j in Seg (i + 1) holds c . j = b . j ) ) i + 1 < (len (the_arity_of o)) + 1 by A16, NAT_1:13; then consider c being Element of Args (o,A) such that A17: c = p . (i + 1) and A18: p . ((i + 1) + 1) = c +* ((i + 1),(b . (i + 1))) by A11, NAT_1:11; i + 1 >= 1 by NAT_1:11; then i + 1 in dom (the_arity_of o) by A16, FINSEQ_3:25; then b . (i + 1) in the Sorts of A . ((the_arity_of o) /. (i + 1)) by A3, Th2; then reconsider d = p . ((i + 1) + 1) as Element of Args (o,A) by A18, Th7; take d ; ::_thesis: ( d = p . ((i + 1) + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > i + 1 holds d . j = a . j ) & ( for j being Nat st j in Seg (i + 1) holds d . j = b . j ) ) thus d = p . ((i + 1) + 1) ; ::_thesis: ( ( for j being Element of NAT st j in dom (the_arity_of o) & j > i + 1 holds d . j = a . j ) & ( for j being Nat st j in Seg (i + 1) holds d . j = b . j ) ) Seg (i + 1) c= dom (the_arity_of o) by A13, A16, FINSEQ_1:5; then A19: Seg (i + 1) c= dom c by MSUALG_3:6; i <= i + 1 by NAT_1:11; then consider ci being Element of Args (o,A) such that A20: ci = p . (i + 1) and A21: for j being Element of NAT st j in dom (the_arity_of o) & j > i holds ci . j = a . j and A22: for j being Nat st j in Seg i holds ci . j = b . j by A15, A16, XXREAL_0:2; hereby ::_thesis: for j being Nat st j in Seg (i + 1) holds d . j = b . j let j be Element of NAT ; ::_thesis: ( j in dom (the_arity_of o) & j > i + 1 implies d . j = a . j ) assume that A23: j in dom (the_arity_of o) and A24: j > i + 1 ; ::_thesis: d . j = a . j j > i by A24, NAT_1:13; then ci . j = a . j by A21, A23; hence d . j = a . j by A20, A17, A18, A24, FUNCT_7:32; ::_thesis: verum end; let j be Nat; ::_thesis: ( j in Seg (i + 1) implies d . j = b . j ) assume A25: j in Seg (i + 1) ; ::_thesis: d . j = b . j then j in (Seg i) \/ {(i + 1)} by FINSEQ_1:9; then A26: ( j in Seg i or j in {(i + 1)} ) by XBOOLE_0:def_3; percases ( j = i + 1 or j <> i + 1 ) ; suppose j = i + 1 ; ::_thesis: d . j = b . j hence d . j = b . j by A18, A25, A19, FUNCT_7:31; ::_thesis: verum end; supposeA27: j <> i + 1 ; ::_thesis: d . j = b . j then d . j = c . j by A18, FUNCT_7:32; hence d . j = b . j by A20, A22, A17, A26, A27, TARSKI:def_1; ::_thesis: verum end; end; end; A28: S2[ 0 ] proof assume 0 <= len (the_arity_of o) ; ::_thesis: ex c being Element of Args (o,A) st ( c = p . (0 + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > 0 holds c . j = a . j ) & ( for j being Nat st j in Seg 0 holds c . j = b . j ) ) take a9 ; ::_thesis: ( a9 = p . (0 + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > 0 holds a9 . j = a . j ) & ( for j being Nat st j in Seg 0 holds a9 . j = b . j ) ) thus ( a9 = p . (0 + 1) & ( for j being Element of NAT st j in dom (the_arity_of o) & j > 0 holds a9 . j = a . j ) & ( for j being Nat st j in Seg 0 holds a9 . j = b . j ) ) by A10; ::_thesis: verum end; A29: for i being Element of NAT holds S2[i] from NAT_1:sch_1(A28, A14); then consider c being Element of Args (o,A) such that A30: c = p . ((len (the_arity_of o)) + 1) and for j being Element of NAT st j in dom (the_arity_of o) & j > len (the_arity_of o) holds c . j = a . j and A31: for j being Nat st j in Seg (len (the_arity_of o)) holds c . j = b . j ; defpred S3[ Element of NAT ] means ( S in dom p implies [((Den (o,A)) . a9),((Den (o,A)) . (p . S))] in R . (the_result_sort_of o) ); A32: for k being Element of NAT st S3[k] holds S3[k + 1] proof A33: Result (o,A) = the Sorts of A . (the_result_sort_of o) by PRALG_2:3; let i be Element of NAT ; ::_thesis: ( S3[i] implies S3[i + 1] ) assume that A34: ( i in dom p implies [((Den (o,A)) . a9),((Den (o,A)) . (p . i))] in R . (the_result_sort_of o) ) and A35: i + 1 in dom p ; ::_thesis: [((Den (o,A)) . a9),((Den (o,A)) . (p . (i + 1)))] in R . (the_result_sort_of o) A36: i + 1 <= len p by A35, FINSEQ_3:25; i <= i + 1 by NAT_1:11; then A37: i <= len p by A36, XXREAL_0:2; percases ( i = 0 or i > 0 ) ; suppose i = 0 ; ::_thesis: [((Den (o,A)) . a9),((Den (o,A)) . (p . (i + 1)))] in R . (the_result_sort_of o) hence [((Den (o,A)) . a9),((Den (o,A)) . (p . (i + 1)))] in R . (the_result_sort_of o) by A10, A33, EQREL_1:5; ::_thesis: verum end; suppose i > 0 ; ::_thesis: [((Den (o,A)) . a9),((Den (o,A)) . (p . (i + 1)))] in R . (the_result_sort_of o) then A38: i >= 0 + 1 by NAT_1:13; then consider j being Nat such that A39: i = 1 + j by NAT_1:10; reconsider j = j as Element of NAT by ORDINAL1:def_12; i < (len (the_arity_of o)) + 1 by A9, A36, NAT_1:13; then consider c being Element of Args (o,A) such that A40: c = p . i and A41: p . (i + 1) = c +* (i,(b . i)) by A11, A38; A42: i <= len (the_arity_of o) by A9, A36, XREAL_1:6; then A43: i in dom (the_arity_of o) by A38, FINSEQ_3:25; then reconsider bi = b . i, ci = c . i as Element of A,((the_arity_of o) /. i) by A3, Th2; j <= i by A39, NAT_1:11; then A44: ex c being Element of Args (o,A) st ( c = p . (j + 1) & ( for k being Element of NAT st k in dom (the_arity_of o) & k > j holds c . k = a . k ) & ( for k being Nat st k in Seg j holds c . k = b . k ) ) by A29, A42, XXREAL_0:2; j < i by A39, NAT_1:13; then c . i = a . i by A40, A43, A39, A44; then A45: [ci,bi] in R . ((the_arity_of o) /. i) by A4, A43; reconsider d = c +* (i,bi) as Element of Args (o,A) by Th7; A46: (Den (o,A)) . d = (transl (o,i,c,A)) . bi by Def4; c = c +* (i,ci) by FUNCT_7:35; then A47: (Den (o,A)) . c = (transl (o,i,c,A)) . ci by Def4; transl (o,i,c,A) is_e.translation_of A,(the_arity_of o) /. i, the_result_sort_of o by A43, Def5; then [((Den (o,A)) . c),((Den (o,A)) . d)] in R . (the_result_sort_of o) by A1, A46, A47, A45; hence [((Den (o,A)) . a9),((Den (o,A)) . (p . (i + 1)))] in R . (the_result_sort_of o) by A34, A37, A38, A40, A41, EQREL_1:7, FINSEQ_3:25; ::_thesis: verum end; end; end; A48: dom b = dom (the_arity_of o) by A3, MSUALG_3:6; then A49: b is FinSequence by A5, FINSEQ_1:def_2; A50: S3[ 0 ] by FINSEQ_3:25; A51: for i being Element of NAT holds S3[i] from NAT_1:sch_1(A50, A32); A52: dom c = dom (the_arity_of o) by MSUALG_3:6; then c is FinSequence by A5, FINSEQ_1:def_2; then c = b by A31, A52, A48, A5, A49, FINSEQ_1:13; hence [((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) by A51, A30, A12; ::_thesis: verum end; cluster MSEquivalence-like compatible -> MSEquivalence-like invariant for ManySortedRelation of the Sorts of A, the Sorts of A; coherence for b1 being MSEquivalence-like ManySortedRelation of A st b1 is compatible holds b1 is invariant proof let R be MSEquivalence-like ManySortedRelation of A; ::_thesis: ( R is compatible implies R is invariant ) assume A53: for o being OperSymbol of S for a, b being Function st a in Args (o,A) & b in Args (o,A) & ( for n being Element of NAT st n in dom (the_arity_of o) holds [(a . n),(b . n)] in R . ((the_arity_of o) /. n) ) holds [((Den (o,A)) . a),((Den (o,A)) . b)] in R . (the_result_sort_of o) ; :: according to MSUALG_6:def_7 ::_thesis: R is invariant let s1, s2 be SortSymbol of S; :: according to MSUALG_6:def_8 ::_thesis: for t being Function st t is_e.translation_of A,s1,s2 holds for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2 let f be Function; ::_thesis: ( f is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) given o being OperSymbol of S such that A54: the_result_sort_of o = s2 and A55: ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st ( a in Args (o,A) & f = transl (o,i,a,A) ) ) ; :: according to MSUALG_6:def_5 ::_thesis: for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 consider i being Element of NAT , a being Function such that i in dom (the_arity_of o) and A56: (the_arity_of o) /. i = s1 and A57: a in Args (o,A) and A58: f = transl (o,i,a,A) by A55; let x, y be set ; ::_thesis: ( [x,y] in R . s1 implies [(f . x),(f . y)] in R . s2 ) assume A59: [x,y] in R . s1 ; ::_thesis: [(f . x),(f . y)] in R . s2 then A60: y in the Sorts of A . s1 by ZFMISC_1:87; A61: x in the Sorts of A . s1 by A59, ZFMISC_1:87; then reconsider ax = a +* (i,x), ay = a +* (i,y) as Element of Args (o,A) by A56, A57, A60, Th7; A62: f . y = (Den (o,A)) . ay by A56, A58, A60, Def4; A63: dom a = dom (the_arity_of o) by A57, MSUALG_3:6; A64: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(the_arity_of_o)_holds_ [(ax_._n),(ay_._n)]_in_R_._((the_arity_of_o)_/._n) let n be Element of NAT ; ::_thesis: ( n in dom (the_arity_of o) implies [(ax . n),(ay . n)] in R . ((the_arity_of o) /. n) ) A65: dom ( the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def_2; assume A66: n in dom (the_arity_of o) ; ::_thesis: [(ax . n),(ay . n)] in R . ((the_arity_of o) /. n) then (the_arity_of o) /. n = (the_arity_of o) . n by PARTFUN1:def_6; then A67: the Sorts of A . ((the_arity_of o) /. n) = ( the Sorts of A * (the_arity_of o)) . n by A66, FUNCT_1:13; ( n = i or n <> i ) ; then ( ( ax . n = x & ay . n = y & n = i ) or ( ax . n = a . n & ay . n = a . n ) ) by A63, A66, FUNCT_7:31, FUNCT_7:32; hence [(ax . n),(ay . n)] in R . ((the_arity_of o) /. n) by A56, A59, A66, A65, A67, EQREL_1:5, MSUALG_3:6; ::_thesis: verum end; f . x = (Den (o,A)) . ax by A56, A58, A61, Def4; hence [(f . x),(f . y)] in R . s2 by A53, A54, A62, A64; ::_thesis: verum end; end; registration let X be non empty set ; cluster id X -> non empty ; coherence not id X is empty ; end; scheme :: MSUALG_6:sch 2 MSRExistence{ F1() -> non empty set , F2() -> V16() ManySortedSet of F1(), P1[ set , set , set ] } : ex R being ManySortedRelation of F2() st for i being Element of F1() for a, b being Element of F2() . i holds ( [a,b] in R . i iff P1[i,a,b] ) proof defpred S1[ set , set ] means P1[\$1,\$2 `1 ,\$2 `2 ]; deffunc H1( set ) -> set = [:(F2() . \$1),(F2() . \$1):]; consider R being Function such that A1: dom R = F1() and A2: for i being set st i in F1() holds for a being set holds ( a in R . i iff ( a in H1(i) & S1[i,a] ) ) from CARD_3:sch_2(); reconsider R = R as ManySortedSet of F1() by A1, PARTFUN1:def_2, RELAT_1:def_18; R is ManySortedRelation of F2() proof let i be set ; :: according to MSUALG_4:def_1 ::_thesis: ( not i in F1() or R . i is Element of bool [:(F2() . i),(F2() . i):] ) assume A3: i in F1() ; ::_thesis: R . i is Element of bool [:(F2() . i),(F2() . i):] R . i c= [:(F2() . i),(F2() . i):] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R . i or x in [:(F2() . i),(F2() . i):] ) thus ( not x in R . i or x in [:(F2() . i),(F2() . i):] ) by A2, A3; ::_thesis: verum end; hence R . i is Element of bool [:(F2() . i),(F2() . i):] ; ::_thesis: verum end; then reconsider R = R as ManySortedRelation of F2() ; take R ; ::_thesis: for i being Element of F1() for a, b being Element of F2() . i holds ( [a,b] in R . i iff P1[i,a,b] ) let i be Element of F1(); ::_thesis: for a, b being Element of F2() . i holds ( [a,b] in R . i iff P1[i,a,b] ) let a, b be Element of F2() . i; ::_thesis: ( [a,b] in R . i iff P1[i,a,b] ) A4: [a,b] `2 = b ; A5: [a,b] in [:(F2() . i),(F2() . i):] by ZFMISC_1:87; [a,b] `1 = a ; hence ( [a,b] in R . i iff P1[i,a,b] ) by A2, A4, A5; ::_thesis: verum end; scheme :: MSUALG_6:sch 3 MSRLambdaU{ F1() -> set , F2() -> ManySortedSet of F1(), F3( set ) -> set } : ( ex R being ManySortedRelation of F2() st for i being set st i in F1() holds R . i = F3(i) & ( for R1, R2 being ManySortedRelation of F2() st ( for i being set st i in F1() holds R1 . i = F3(i) ) & ( for i being set st i in F1() holds R2 . i = F3(i) ) holds R1 = R2 ) ) provided A1: for i being set st i in F1() holds F3(i) is Relation of (F2() . i),(F2() . i) proof consider R being ManySortedSet of F1() such that A2: for i being set st i in F1() holds R . i = F3(i) from PBOOLE:sch_4(); R is ManySortedRelation of F2() proof let i be set ; :: according to MSUALG_4:def_1 ::_thesis: ( not i in F1() or R . i is Element of bool [:(F2() . i),(F2() . i):] ) assume A3: i in F1() ; ::_thesis: R . i is Element of bool [:(F2() . i),(F2() . i):] then F3(i) is Relation of (F2() . i),(F2() . i) by A1; hence R . i is Element of bool [:(F2() . i),(F2() . i):] by A2, A3; ::_thesis: verum end; hence ex R being ManySortedRelation of F2() st for i being set st i in F1() holds R . i = F3(i) by A2; ::_thesis: for R1, R2 being ManySortedRelation of F2() st ( for i being set st i in F1() holds R1 . i = F3(i) ) & ( for i being set st i in F1() holds R2 . i = F3(i) ) holds R1 = R2 let R1, R2 be ManySortedRelation of F2(); ::_thesis: ( ( for i being set st i in F1() holds R1 . i = F3(i) ) & ( for i being set st i in F1() holds R2 . i = F3(i) ) implies R1 = R2 ) assume that A4: for i being set st i in F1() holds R1 . i = F3(i) and A5: for i being set st i in F1() holds R2 . i = F3(i) ; ::_thesis: R1 = R2 now__::_thesis:_for_i_being_set_st_i_in_F1()_holds_ R1_._i_=_R2_._i let i be set ; ::_thesis: ( i in F1() implies R1 . i = R2 . i ) assume A6: i in F1() ; ::_thesis: R1 . i = R2 . i then R1 . i = F3(i) by A4; hence R1 . i = R2 . i by A5, A6; ::_thesis: verum end; hence R1 = R2 by PBOOLE:3; ::_thesis: verum end; definition let I be set ; let A be ManySortedSet of I; func id (I,A) -> ManySortedRelation of A means :Def10: :: MSUALG_6:def 10 for i being set st i in I holds it . i = id (A . i); correctness existence ex b1 being ManySortedRelation of A st for i being set st i in I holds b1 . i = id (A . i); uniqueness for b1, b2 being ManySortedRelation of A st ( for i being set st i in I holds b1 . i = id (A . i) ) & ( for i being set st i in I holds b2 . i = id (A . i) ) holds b1 = b2; proof deffunc H1( set ) -> Element of bool [:(A . \$1),(A . \$1):] = id (A . \$1); A1: for i being set st i in I holds H1(i) is Relation of (A . i),(A . i) ; ( ex R being ManySortedRelation of A st for i being set st i in I holds R . i = H1(i) & ( for R1, R2 being ManySortedRelation of A st ( for i being set st i in I holds R1 . i = H1(i) ) & ( for i being set st i in I holds R2 . i = H1(i) ) holds R1 = R2 ) ) from MSUALG_6:sch_3(A1); hence ( ex b1 being ManySortedRelation of A st for i being set st i in I holds b1 . i = id (A . i) & ( for b1, b2 being ManySortedRelation of A st ( for i being set st i in I holds b1 . i = id (A . i) ) & ( for i being set st i in I holds b2 . i = id (A . i) ) holds b1 = b2 ) ) ; ::_thesis: verum end; end; :: deftheorem Def10 defines id MSUALG_6:def_10_:_ for I being set for A being ManySortedSet of I for b3 being ManySortedRelation of A holds ( b3 = id (I,A) iff for i being set st i in I holds b3 . i = id (A . i) ); registration let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; cluster MSEquivalence-like -> V16() for ManySortedRelation of the Sorts of A, the Sorts of A; coherence for b1 being ManySortedRelation of A st b1 is MSEquivalence-like holds b1 is V16() proof let R be ManySortedRelation of A; ::_thesis: ( R is MSEquivalence-like implies R is V16() ) assume A1: for i being set for P being Relation of ( the Sorts of A . i) st i in the carrier of S & R . i = P holds P is Equivalence_Relation of ( the Sorts of A . i) ; :: according to MSUALG_4:def_2,MSUALG_4:def_3 ::_thesis: R is V16() let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in the carrier of S or not R . i is empty ) assume i in the carrier of S ; ::_thesis: not R . i is empty then reconsider i = i as SortSymbol of S ; R . i is Equivalence_Relation of ( the Sorts of A . i) by A1; hence not R . i is empty ; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like invariant stable for ManySortedRelation of the Sorts of A, the Sorts of A; existence ex b1 being ManySortedRelation of A st ( b1 is invariant & b1 is stable & b1 is MSEquivalence-like ) proof reconsider R = id ( the carrier of S, the Sorts of A) as ManySortedRelation of A ; take R ; ::_thesis: ( R is invariant & R is stable & R is MSEquivalence-like ) thus R is invariant ::_thesis: ( R is stable & R is MSEquivalence-like ) proof let s1, s2 be SortSymbol of S; :: according to MSUALG_6:def_8 ::_thesis: for t being Function st t is_e.translation_of A,s1,s2 holds for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2 let t be Function; ::_thesis: ( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2 ) assume t is_e.translation_of A,s1,s2 ; ::_thesis: for a, b being set st [a,b] in R . s1 holds [(t . a),(t . b)] in R . s2 then reconsider f = t as Function of ( the Sorts of A . s1),( the Sorts of A . s2) by Th11; let a, b be set ; ::_thesis: ( [a,b] in R . s1 implies [(t . a),(t . b)] in R . s2 ) assume A1: [a,b] in R . s1 ; ::_thesis: [(t . a),(t . b)] in R . s2 then a in the Sorts of A . s1 by ZFMISC_1:87; then A2: f . a in the Sorts of A . s2 by FUNCT_2:5; R . s1 = id ( the Sorts of A . s1) by Def10; then A3: a = b by A1, RELAT_1:def_10; R . s2 = id ( the Sorts of A . s2) by Def10; hence [(t . a),(t . b)] in R . s2 by A3, A2, RELAT_1:def_10; ::_thesis: verum end; thus R is stable ::_thesis: R is MSEquivalence-like proof let h be Endomorphism of A; :: according to MSUALG_6:def_9 ::_thesis: for s being SortSymbol of S for a, b being set st [a,b] in R . s holds [((h . s) . a),((h . s) . b)] in R . s let s be SortSymbol of S; ::_thesis: for a, b being set st [a,b] in R . s holds [((h . s) . a),((h . s) . b)] in R . s let a, b be set ; ::_thesis: ( [a,b] in R . s implies [((h . s) . a),((h . s) . b)] in R . s ) A4: R . s = id ( the Sorts of A . s) by Def10; assume A5: [a,b] in R . s ; ::_thesis: [((h . s) . a),((h . s) . b)] in R . s then a in the Sorts of A . s by A4, RELAT_1:def_10; then A6: (h . s) . a in the Sorts of A . s by FUNCT_2:5; a = b by A4, A5, RELAT_1:def_10; hence [((h . s) . a),((h . s) . b)] in R . s by A4, A6, RELAT_1:def_10; ::_thesis: verum end; 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 R . i = b1 or b1 is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] ) let P be Relation of ( the Sorts of A . i); ::_thesis: ( not i in the carrier of S or not R . i = P or P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] ) assume i in the carrier of S ; ::_thesis: ( not R . i = P or P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] ) then reconsider s = i as SortSymbol of S ; assume R . i = P ; ::_thesis: P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] then P = id ( the Sorts of A . s) by Def10; hence P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] ; ::_thesis: verum end; end; begin scheme :: MSUALG_6:sch 4 MSRelCl{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), P1[ set , set , set ], P2[ set ], F3() -> ManySortedRelation of F2(), F4() -> ManySortedRelation of F2() } : ( P2[F4()] & F3() c= F4() & ( for P being ManySortedRelation of F2() st P2[P] & F3() c= P holds F4() c= P ) ) provided A1: for R being ManySortedRelation of F2() holds ( P2[R] iff for s1, s2 being SortSymbol of F1() for f being Function of ( the Sorts of F2() . s1),( the Sorts of F2() . s2) st P1[f,s1,s2] holds for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) and A2: for s1, s2, s3 being SortSymbol of F1() for f1 being Function of ( the Sorts of F2() . s1),( the Sorts of F2() . s2) for f2 being Function of ( the Sorts of F2() . s2),( the Sorts of F2() . s3) st P1[f1,s1,s2] & P1[f2,s2,s3] holds P1[f2 * f1,s1,s3] and A3: for s being SortSymbol of F1() holds P1[ id ( the Sorts of F2() . s),s,s] and A4: for s being SortSymbol of F1() for a, b being Element of F2(),s holds ( [a,b] in F4() . s iff ex s9 being SortSymbol of F1() ex f being Function of ( the Sorts of F2() . s9),( the Sorts of F2() . s) ex x, y being Element of F2(),s9 st ( P1[f,s9,s] & [x,y] in F3() . s9 & a = f . x & b = f . y ) ) proof now__::_thesis:_for_s1,_s2_being_SortSymbol_of_F1() for_f_being_Function_of_(_the_Sorts_of_F2()_._s1),(_the_Sorts_of_F2()_._s2)_st_P1[f,s1,s2]_holds_ for_a,_b_being_set_st_[a,b]_in_F4()_._s1_holds_ [(f_._a),(f_._b)]_in_F4()_._s2 let s1, s2 be SortSymbol of F1(); ::_thesis: for f being Function of ( the Sorts of F2() . s1),( the Sorts of F2() . s2) st P1[f,s1,s2] holds for a, b being set st [a,b] in F4() . s1 holds [(f . a),(f . b)] in F4() . s2 set R = F4(); let f be Function of ( the Sorts of F2() . s1),( the Sorts of F2() . s2); ::_thesis: ( P1[f,s1,s2] implies for a, b being set st [a,b] in F4() . s1 holds [(f . a),(f . b)] in F4() . s2 ) assume A5: P1[f,s1,s2] ; ::_thesis: for a, b being set st [a,b] in F4() . s1 holds [(f . a),(f . b)] in F4() . s2 let a, b be set ; ::_thesis: ( [a,b] in F4() . s1 implies [(f . a),(f . b)] in F4() . s2 ) assume A6: [a,b] in F4() . s1 ; ::_thesis: [(f . a),(f . b)] in F4() . s2 then A7: b in the Sorts of F2() . s1 by ZFMISC_1:87; a in the Sorts of F2() . s1 by A6, ZFMISC_1:87; then consider s9 being SortSymbol of F1(), f9 being Function of ( the Sorts of F2() . s9),( the Sorts of F2() . s1), x, y being Element of F2(),s9 such that A8: P1[f9,s9,s1] and A9: [x,y] in F3() . s9 and A10: a = f9 . x and A11: b = f9 . y by A4, A6, A7; A12: f . a = (f * f9) . x by A10, FUNCT_2:15; A13: f . b = (f * f9) . y by A11, FUNCT_2:15; P1[f * f9,s9,s2] by A2, A5, A8; hence [(f . a),(f . b)] in F4() . s2 by A4, A9, A12, A13; ::_thesis: verum end; hence P2[F4()] by A1; ::_thesis: ( F3() c= F4() & ( for P being ManySortedRelation of F2() st P2[P] & F3() c= P holds F4() c= P ) ) thus F3() c= F4() ::_thesis: for P being ManySortedRelation of F2() st P2[P] & F3() c= P holds F4() c= P proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of F1() or F3() . i c= F4() . i ) assume i in the carrier of F1() ; ::_thesis: F3() . i c= F4() . i then reconsider s = i as SortSymbol of F1() ; F3() . s c= F4() . s proof set f = id ( the Sorts of F2() . s); let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in F3() . s or [x,y] in F4() . s ) assume A14: [x,y] in F3() . s ; ::_thesis: [x,y] in F4() . s then reconsider a = x, b = y as Element of F2(),s by ZFMISC_1:87; A15: (id ( the Sorts of F2() . s)) . b = b by FUNCT_1:17; A16: P1[ id ( the Sorts of F2() . s),s,s] by A3; (id ( the Sorts of F2() . s)) . a = a by FUNCT_1:17; hence [x,y] in F4() . s by A4, A14, A16, A15; ::_thesis: verum end; hence F3() . i c= F4() . i ; ::_thesis: verum end; let P be ManySortedRelation of F2(); ::_thesis: ( P2[P] & F3() c= P implies F4() c= P ) assume that A17: P2[P] and A18: F3() c= P ; ::_thesis: F4() c= P let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of F1() or F4() . i c= P . i ) assume i in the carrier of F1() ; ::_thesis: F4() . i c= P . i then reconsider s = i as SortSymbol of F1() ; F4() . s c= P . s proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in F4() . s or [x,y] in P . s ) assume A19: [x,y] in F4() . s ; ::_thesis: [x,y] in P . s then reconsider a = x, b = y as Element of F2(),s by ZFMISC_1:87; consider s9 being SortSymbol of F1(), f being Function of ( the Sorts of F2() . s9),( the Sorts of F2() . s), u, v being Element of F2(),s9 such that A20: P1[f,s9,s] and A21: [u,v] in F3() . s9 and A22: a = f . u and A23: b = f . v by A4, A19; F3() . s9 c= P . s9 by A18, PBOOLE:def_2; hence [x,y] in P . s by A1, A17, A20, A21, A22, A23; ::_thesis: verum end; hence F4() . i c= P . i ; ::_thesis: verum end; Lm1: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_ for_A_being_non-empty_MSAlgebra_over_S for_R,_Q_being_ManySortedRelation_of_A_st_(_for_s_being_SortSymbol_of_S for_a,_b_being_Element_of_A,s_holds_ (_[a,b]_in_Q_._s_iff_ex_s9_being_SortSymbol_of_S_ex_f_being_Function_of_(_the_Sorts_of_A_._s9),(_the_Sorts_of_A_._s)_ex_x,_y_being_Element_of_A,s9_st_ (_S2[f,s9,s]_&_[x,y]_in_R_._s9_&_a_=_f_._x_&_b_=_f_._y_)_)_)_holds_ (_S1[Q]_&_R_c=_Q_&_(_for_P_being_ManySortedRelation_of_A_st_S1[P]_&_R_c=_P_holds_ Q_c=_P_)_) let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st ( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds Q c= P ) ) let A be non-empty MSAlgebra over S; ::_thesis: for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st ( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds Q c= P ) ) let R, Q be ManySortedRelation of A; ::_thesis: ( ( for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st ( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) implies ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds Q c= P ) ) ) defpred S1[ ManySortedRelation of A] means \$1 is invariant ; defpred S2[ Function, SortSymbol of S, SortSymbol of S] means ( TranslationRel S reduces \$2,\$3 & \$1 is Translation of A,\$2,\$3 ); assume A1: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st ( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ; ::_thesis: ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds Q c= P ) ) A2: for s being SortSymbol of S holds S2[ id ( the Sorts of A . s),s,s] by Th16, REWRITE1:12; A3: now__::_thesis:_for_R_being_ManySortedRelation_of_A_holds_ (_(_S1[R]_implies_for_s1,_s2_being_SortSymbol_of_S for_f_being_Function_of_(_the_Sorts_of_A_._s1),(_the_Sorts_of_A_._s2)_st_S2[f,s1,s2]_holds_ for_a,_b_being_set_st_[a,b]_in_R_._s1_holds_ [(f_._a),(f_._b)]_in_R_._s2_)_&_(_(_for_s1,_s2_being_SortSymbol_of_S for_f_being_Function_of_(_the_Sorts_of_A_._s1),(_the_Sorts_of_A_._s2)_st_S2[f,s1,s2]_holds_ for_a,_b_being_set_st_[a,b]_in_R_._s1_holds_ [(f_._a),(f_._b)]_in_R_._s2_)_implies_S1[R]_)_) let R be ManySortedRelation of A; ::_thesis: ( ( S1[R] implies for s1, s2 being SortSymbol of S for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) & ( ( for s1, s2 being SortSymbol of S for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) implies S1[R] ) ) thus ( S1[R] implies for s1, s2 being SortSymbol of S for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) by Th28; ::_thesis: ( ( for s1, s2 being SortSymbol of S for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) implies S1[R] ) assume for s1, s2 being SortSymbol of S for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ; ::_thesis: S1[R] then for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds for f being Translation of A,s1,s2 for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ; hence S1[R] by Th28; ::_thesis: verum end; A4: for s1, s2, s3 being SortSymbol of S for f1 being Function of ( the Sorts of A . s1),( the Sorts of A . s2) for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S2[f1,s1,s2] & S2[f2,s2,s3] holds S2[f2 * f1,s1,s3] by Th18, REWRITE1:16; thus ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds Q c= P ) ) from MSUALG_6:sch_4(A3, A4, A2, A1); ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let R be ManySortedRelation of the Sorts of A; func InvCl R -> invariant ManySortedRelation of A means :Def11: :: MSUALG_6:def 11 ( R c= it & ( for Q being invariant ManySortedRelation of A st R c= Q holds it c= Q ) ); uniqueness for b1, b2 being invariant ManySortedRelation of A st R c= b1 & ( for Q being invariant ManySortedRelation of A st R c= Q holds b1 c= Q ) & R c= b2 & ( for Q being invariant ManySortedRelation of A st R c= Q holds b2 c= Q ) holds b1 = b2 proof let Q1, Q2 be invariant ManySortedRelation of A; ::_thesis: ( R c= Q1 & ( for Q being invariant ManySortedRelation of A st R c= Q holds Q1 c= Q ) & R c= Q2 & ( for Q being invariant ManySortedRelation of A st R c= Q holds Q2 c= Q ) implies Q1 = Q2 ) assume that A1: R c= Q1 and A2: for Q being invariant ManySortedRelation of A st R c= Q holds Q1 c= Q and A3: R c= Q2 and A4: for Q being invariant ManySortedRelation of A st R c= Q holds Q2 c= Q ; ::_thesis: Q1 = Q2 ( Q1 c= Q2 & Q2 c= Q1 ) by A1, A2, A3, A4; hence Q1 = Q2 by PBOOLE:146; ::_thesis: verum end; existence ex b1 being invariant ManySortedRelation of A st ( R c= b1 & ( for Q being invariant ManySortedRelation of A st R c= Q holds b1 c= Q ) ) proof defpred S1[ Function, SortSymbol of S, SortSymbol of S] means ( TranslationRel S reduces \$2,\$3 & \$1 is Translation of A,\$2,\$3 ); defpred S2[ SortSymbol of S, set , set ] means ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . \$1) ex x, y being Element of A,s9 st ( S1[f,s9,\$1] & [x,y] in R . s9 & \$2 = f . x & \$3 = f . y ); consider Q being ManySortedRelation of the Sorts of A such that A5: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff S2[s,a,b] ) from MSUALG_6:sch_2(); reconsider Q = Q as ManySortedRelation of A ; reconsider Q = Q as invariant ManySortedRelation of A by A5, Lm1; take Q ; ::_thesis: ( R c= Q & ( for Q being invariant ManySortedRelation of A st R c= Q holds Q c= Q ) ) thus ( R c= Q & ( for Q being invariant ManySortedRelation of A st R c= Q holds Q c= Q ) ) by A5, Lm1; ::_thesis: verum end; end; :: deftheorem Def11 defines InvCl MSUALG_6:def_11_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A for b4 being invariant ManySortedRelation of A holds ( b4 = InvCl R iff ( R c= b4 & ( for Q being invariant ManySortedRelation of A st R c= Q holds b4 c= Q ) ) ); theorem Th29: :: MSUALG_6:29 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (InvCl R) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st ( TranslationRel S reduces s9,s & [x,y] in R . s9 & a = t . x & b = t . y ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (InvCl R) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st ( TranslationRel S reduces s9,s & [x,y] in R . s9 & a = t . x & b = t . y ) ) let A be non-empty MSAlgebra over S; ::_thesis: for R being ManySortedRelation of the Sorts of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (InvCl R) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st ( TranslationRel S reduces s9,s & [x,y] in R . s9 & a = t . x & b = t . y ) ) let P be ManySortedRelation of the Sorts of A; ::_thesis: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (InvCl P) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st ( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) ) defpred S1[ SortSymbol of S, set , set ] means ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . \$1) ex x, y being Element of A,s9 st ( TranslationRel S reduces s9,\$1 & f is Translation of A,s9,\$1 & [x,y] in P . s9 & \$2 = f . x & \$3 = f . y ); let s be SortSymbol of S; ::_thesis: for a, b being Element of A,s holds ( [a,b] in (InvCl P) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st ( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) ) let a, b be Element of A,s; ::_thesis: ( [a,b] in (InvCl P) . s iff ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st ( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) ) consider Q being ManySortedRelation of the Sorts of A such that A1: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff S1[s,a,b] ) from MSUALG_6:sch_2(); reconsider R = P, Q = Q as ManySortedRelation of A ; A2: R c= Q by A1, Lm1; reconsider Q = Q as invariant ManySortedRelation of A by A1, Lm1; R c= InvCl R by Def11; then A3: Q c= InvCl R by A1, Lm1; InvCl R c= Q by A2, Def11; then A4: InvCl R = Q by A3, PBOOLE:146; hereby ::_thesis: ( ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st ( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) implies [a,b] in (InvCl P) . s ) assume [a,b] in (InvCl P) . s ; ::_thesis: ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st ( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) then ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st ( TranslationRel S reduces s9,s & f is Translation of A,s9,s & [x,y] in P . s9 & a = f . x & b = f . y ) by A1, A4; hence ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st ( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) ; ::_thesis: verum end; thus ( ex s9 being SortSymbol of S ex x, y being Element of A,s9 ex t being Translation of A,s9,s st ( TranslationRel S reduces s9,s & [x,y] in P . s9 & a = t . x & b = t . y ) implies [a,b] in (InvCl P) . s ) by A1, A4; ::_thesis: verum end; theorem Th30: :: MSUALG_6:30 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being stable ManySortedRelation of A holds InvCl R is stable proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being stable ManySortedRelation of A holds InvCl R is stable let A be non-empty MSAlgebra over S; ::_thesis: for R being stable ManySortedRelation of A holds InvCl R is stable let R be stable ManySortedRelation of A; ::_thesis: InvCl R is stable let h be Endomorphism of A; :: according to MSUALG_6:def_9 ::_thesis: for s being SortSymbol of S for a, b being set st [a,b] in (InvCl R) . s holds [((h . s) . a),((h . s) . b)] in (InvCl R) . s let s be SortSymbol of S; ::_thesis: for a, b being set st [a,b] in (InvCl R) . s holds [((h . s) . a),((h . s) . b)] in (InvCl R) . s let a, b be set ; ::_thesis: ( [a,b] in (InvCl R) . s implies [((h . s) . a),((h . s) . b)] in (InvCl R) . s ) assume A1: [a,b] in (InvCl R) . s ; ::_thesis: [((h . s) . a),((h . s) . b)] in (InvCl R) . s then A2: b in the Sorts of A . s by ZFMISC_1:87; a in the Sorts of A . s by A1, ZFMISC_1:87; then consider s9 being SortSymbol of S, x, y being Element of A,s9, t being Translation of A,s9,s such that A3: TranslationRel S reduces s9,s and A4: [x,y] in R . s9 and A5: a = t . x and A6: b = t . y by A1, A2, Th29; consider T being Translation of A,s9,s such that A7: T * (h . s9) = (h . s) * t by A3, Th26; (T * (h . s9)) . y = T . ((h . s9) . y) by FUNCT_2:15; then A8: T . ((h . s9) . y) = (h . s) . b by A6, A7, FUNCT_2:15; (T * (h . s9)) . x = T . ((h . s9) . x) by FUNCT_2:15; then A9: T . ((h . s9) . x) = (h . s) . a by A5, A7, FUNCT_2:15; [((h . s9) . x),((h . s9) . y)] in R . s9 by A4, Def9; hence [((h . s) . a),((h . s) . b)] in (InvCl R) . s by A3, A9, A8, Th29; ::_thesis: verum end; Lm2: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_ for_A_being_non-empty_MSAlgebra_over_S for_R,_Q_being_ManySortedRelation_of_A_st_(_for_s_being_SortSymbol_of_S for_a,_b_being_Element_of_A,s_holds_ (_[a,b]_in_Q_._s_iff_ex_s9_being_SortSymbol_of_S_ex_f_being_Function_of_(_the_Sorts_of_A_._s9),(_the_Sorts_of_A_._s)_ex_x,_y_being_Element_of_A,s9_st_ (_S2[f,s9,s]_&_[x,y]_in_R_._s9_&_a_=_f_._x_&_b_=_f_._y_)_)_)_holds_ (_S1[Q]_&_R_c=_Q_&_(_for_P_being_ManySortedRelation_of_A_st_S1[P]_&_R_c=_P_holds_ Q_c=_P_)_) let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st ( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds Q c= P ) ) let A be non-empty MSAlgebra over S; ::_thesis: for R, Q being ManySortedRelation of A st ( for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st ( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) holds ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds Q c= P ) ) let R, Q be ManySortedRelation of A; ::_thesis: ( ( for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st ( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ) implies ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds Q c= P ) ) ) defpred S1[ ManySortedRelation of A] means \$1 is stable ; defpred S2[ Function, SortSymbol of S, SortSymbol of S] means ( \$2 = \$3 & ex h being Endomorphism of A st \$1 = h . \$2 ); A1: for s1, s2, s3 being SortSymbol of S for f1 being Function of ( the Sorts of A . s1),( the Sorts of A . s2) for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S2[f1,s1,s2] & S2[f2,s2,s3] holds S2[f2 * f1,s1,s3] proof let s1, s2, s3 be SortSymbol of S; ::_thesis: for f1 being Function of ( the Sorts of A . s1),( the Sorts of A . s2) for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S2[f1,s1,s2] & S2[f2,s2,s3] holds S2[f2 * f1,s1,s3] let f1 be Function of ( the Sorts of A . s1),( the Sorts of A . s2); ::_thesis: for f2 being Function of ( the Sorts of A . s2),( the Sorts of A . s3) st S2[f1,s1,s2] & S2[f2,s2,s3] holds S2[f2 * f1,s1,s3] let f2 be Function of ( the Sorts of A . s2),( the Sorts of A . s3); ::_thesis: ( S2[f1,s1,s2] & S2[f2,s2,s3] implies S2[f2 * f1,s1,s3] ) assume A2: s1 = s2 ; ::_thesis: ( for h being Endomorphism of A holds not f1 = h . s1 or not S2[f2,s2,s3] or S2[f2 * f1,s1,s3] ) given h1 being Endomorphism of A such that A3: f1 = h1 . s1 ; ::_thesis: ( not S2[f2,s2,s3] or S2[f2 * f1,s1,s3] ) assume A4: s2 = s3 ; ::_thesis: ( for h being Endomorphism of A holds not f2 = h . s2 or S2[f2 * f1,s1,s3] ) given h2 being Endomorphism of A such that A5: f2 = h2 . s2 ; ::_thesis: S2[f2 * f1,s1,s3] thus s1 = s3 by A2, A4; ::_thesis: ex h being Endomorphism of A st f2 * f1 = h . s1 reconsider h = h2 ** h1 as Endomorphism of A ; take h ; ::_thesis: f2 * f1 = h . s1 thus f2 * f1 = h . s1 by A2, A3, A5, MSUALG_3:2; ::_thesis: verum end; A6: for R being ManySortedRelation of A holds ( S1[R] iff for s1, s2 being SortSymbol of S for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) proof let R be ManySortedRelation of A; ::_thesis: ( S1[R] iff for s1, s2 being SortSymbol of S for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) thus ( R is stable implies for s1, s2 being SortSymbol of S for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st s1 = s2 & ex h being Endomorphism of A st f = h . s1 holds for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) by Def9; ::_thesis: ( ( for s1, s2 being SortSymbol of S for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ) implies S1[R] ) assume A7: for s1, s2 being SortSymbol of S for f being Function of ( the Sorts of A . s1),( the Sorts of A . s2) st S2[f,s1,s2] holds for a, b being set st [a,b] in R . s1 holds [(f . a),(f . b)] in R . s2 ; ::_thesis: S1[R] thus R is stable ::_thesis: verum proof let h be Endomorphism of A; :: according to MSUALG_6:def_9 ::_thesis: for s being SortSymbol of S for a, b being set st [a,b] in R . s holds [((h . s) . a),((h . s) . b)] in R . s let s be SortSymbol of S; ::_thesis: for a, b being set st [a,b] in R . s holds [((h . s) . a),((h . s) . b)] in R . s thus for a, b being set st [a,b] in R . s holds [((h . s) . a),((h . s) . b)] in R . s by A7; ::_thesis: verum end; end; A8: for s being SortSymbol of S holds S2[ id ( the Sorts of A . s),s,s] proof reconsider h = id the Sorts of A as Endomorphism of A by Th4; let s be SortSymbol of S; ::_thesis: S2[ id ( the Sorts of A . s),s,s] thus s = s ; ::_thesis: ex h being Endomorphism of A st id ( the Sorts of A . s) = h . s take h ; ::_thesis: id ( the Sorts of A . s) = h . s thus id ( the Sorts of A . s) = h . s by MSUALG_3:def_1; ::_thesis: verum end; assume A9: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st ( S2[f,s9,s] & [x,y] in R . s9 & a = f . x & b = f . y ) ) ; ::_thesis: ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds Q c= P ) ) thus ( S1[Q] & R c= Q & ( for P being ManySortedRelation of A st S1[P] & R c= P holds Q c= P ) ) from MSUALG_6:sch_4(A6, A1, A8, A9); ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let R be ManySortedRelation of the Sorts of A; func StabCl R -> stable ManySortedRelation of A means :Def12: :: MSUALG_6:def 12 ( R c= it & ( for Q being stable ManySortedRelation of A st R c= Q holds it c= Q ) ); uniqueness for b1, b2 being stable ManySortedRelation of A st R c= b1 & ( for Q being stable ManySortedRelation of A st R c= Q holds b1 c= Q ) & R c= b2 & ( for Q being stable ManySortedRelation of A st R c= Q holds b2 c= Q ) holds b1 = b2 proof let Q1, Q2 be stable ManySortedRelation of A; ::_thesis: ( R c= Q1 & ( for Q being stable ManySortedRelation of A st R c= Q holds Q1 c= Q ) & R c= Q2 & ( for Q being stable ManySortedRelation of A st R c= Q holds Q2 c= Q ) implies Q1 = Q2 ) assume that A1: R c= Q1 and A2: for Q being stable ManySortedRelation of A st R c= Q holds Q1 c= Q and A3: R c= Q2 and A4: for Q being stable ManySortedRelation of A st R c= Q holds Q2 c= Q ; ::_thesis: Q1 = Q2 ( Q1 c= Q2 & Q2 c= Q1 ) by A1, A2, A3, A4; hence Q1 = Q2 by PBOOLE:146; ::_thesis: verum end; existence ex b1 being stable ManySortedRelation of A st ( R c= b1 & ( for Q being stable ManySortedRelation of A st R c= Q holds b1 c= Q ) ) proof defpred S1[ Function, SortSymbol of S, SortSymbol of S] means ( \$2 = \$3 & ex h being Endomorphism of A st \$1 = h . \$2 ); defpred S2[ SortSymbol of S, set , set ] means ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . \$1) ex x, y being Element of A,s9 st ( S1[f,s9,\$1] & [x,y] in R . s9 & \$2 = f . x & \$3 = f . y ); consider Q being ManySortedRelation of the Sorts of A such that A5: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff S2[s,a,b] ) from MSUALG_6:sch_2(); reconsider Q = Q as ManySortedRelation of A ; reconsider Q = Q as stable ManySortedRelation of A by A5, Lm2; take Q ; ::_thesis: ( R c= Q & ( for Q being stable ManySortedRelation of A st R c= Q holds Q c= Q ) ) thus ( R c= Q & ( for Q being stable ManySortedRelation of A st R c= Q holds Q c= Q ) ) by A5, Lm2; ::_thesis: verum end; end; :: deftheorem Def12 defines StabCl MSUALG_6:def_12_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A for b4 being stable ManySortedRelation of A holds ( b4 = StabCl R iff ( R c= b4 & ( for Q being stable ManySortedRelation of A st R c= Q holds b4 c= Q ) ) ); theorem Th31: :: MSUALG_6:31 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (StabCl R) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st ( [x,y] in R . s & a = (h . s) . x & b = (h . s) . y ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (StabCl R) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st ( [x,y] in R . s & a = (h . s) . x & b = (h . s) . y ) ) let A be non-empty MSAlgebra over S; ::_thesis: for R being ManySortedRelation of the Sorts of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (StabCl R) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st ( [x,y] in R . s & a = (h . s) . x & b = (h . s) . y ) ) let P be ManySortedRelation of the Sorts of A; ::_thesis: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (StabCl P) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st ( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) ) defpred S1[ SortSymbol of S, set , set ] means ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . \$1) ex x, y being Element of A,s9 st ( s9 = \$1 & ex h being Endomorphism of A st f = h . s9 & [x,y] in P . s9 & \$2 = f . x & \$3 = f . y ); let s be SortSymbol of S; ::_thesis: for a, b being Element of A,s holds ( [a,b] in (StabCl P) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st ( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) ) let a, b be Element of A,s; ::_thesis: ( [a,b] in (StabCl P) . s iff ex x, y being Element of A,s ex h being Endomorphism of A st ( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) ) consider Q being ManySortedRelation of the Sorts of A such that A1: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in Q . s iff S1[s,a,b] ) from MSUALG_6:sch_2(); reconsider R = P, Q = Q as ManySortedRelation of A ; A2: R c= Q by A1, Lm2; reconsider Q = Q as stable ManySortedRelation of A by A1, Lm2; R c= StabCl R by Def12; then A3: Q c= StabCl R by A1, Lm2; StabCl R c= Q by A2, Def12; then A4: StabCl R = Q by A3, PBOOLE:146; hereby ::_thesis: ( ex x, y being Element of A,s ex h being Endomorphism of A st ( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) implies [a,b] in (StabCl P) . s ) assume [a,b] in (StabCl P) . s ; ::_thesis: ex x, y being Element of A,s ex h being Endomorphism of A st ( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) then ex s9 being SortSymbol of S ex f being Function of ( the Sorts of A . s9),( the Sorts of A . s) ex x, y being Element of A,s9 st ( s9 = s & ex h being Endomorphism of A st f = h . s9 & [x,y] in P . s9 & a = f . x & b = f . y ) by A1, A4; hence ex x, y being Element of A,s ex h being Endomorphism of A st ( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) ; ::_thesis: verum end; thus ( ex x, y being Element of A,s ex h being Endomorphism of A st ( [x,y] in P . s & a = (h . s) . x & b = (h . s) . y ) implies [a,b] in (StabCl P) . s ) by A1, A4; ::_thesis: verum end; theorem :: MSUALG_6:32 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) is stable by Th30; definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let R be ManySortedRelation of the Sorts of A; func TRS R -> invariant stable ManySortedRelation of A means :Def13: :: MSUALG_6:def 13 ( R c= it & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds it c= Q ) ); uniqueness for b1, b2 being invariant stable ManySortedRelation of A st R c= b1 & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds b1 c= Q ) & R c= b2 & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds b2 c= Q ) holds b1 = b2 proof let Q1, Q2 be invariant stable ManySortedRelation of A; ::_thesis: ( R c= Q1 & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds Q1 c= Q ) & R c= Q2 & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds Q2 c= Q ) implies Q1 = Q2 ) assume that A1: R c= Q1 and A2: for Q being invariant stable ManySortedRelation of A st R c= Q holds Q1 c= Q and A3: R c= Q2 and A4: for Q being invariant stable ManySortedRelation of A st R c= Q holds Q2 c= Q ; ::_thesis: Q1 = Q2 ( Q1 c= Q2 & Q2 c= Q1 ) by A1, A2, A3, A4; hence Q1 = Q2 by PBOOLE:146; ::_thesis: verum end; existence ex b1 being invariant stable ManySortedRelation of A st ( R c= b1 & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds b1 c= Q ) ) proof reconsider Q = InvCl (StabCl R) as invariant stable ManySortedRelation of A by Th30; take Q ; ::_thesis: ( R c= Q & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds Q c= Q ) ) A5: StabCl R c= InvCl (StabCl R) by Def11; R c= StabCl R by Def12; hence R c= Q by A5, PBOOLE:13; ::_thesis: for Q being invariant stable ManySortedRelation of A st R c= Q holds Q c= Q let P be invariant stable ManySortedRelation of A; ::_thesis: ( R c= P implies Q c= P ) assume R c= P ; ::_thesis: Q c= P then StabCl R c= P by Def12; hence Q c= P by Def11; ::_thesis: verum end; end; :: deftheorem Def13 defines TRS MSUALG_6:def_13_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A for b4 being invariant stable ManySortedRelation of A holds ( b4 = TRS R iff ( R c= b4 & ( for Q being invariant stable ManySortedRelation of A st R c= Q holds b4 c= Q ) ) ); registration let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let R be V16() ManySortedRelation of A; cluster InvCl R -> V16() invariant ; coherence InvCl R is non-empty proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in the carrier of S or not (InvCl R) . i is empty ) assume i in the carrier of S ; ::_thesis: not (InvCl R) . i is empty then reconsider s = i as SortSymbol of S ; set x = the Element of R . s; R c= InvCl R by Def11; then A1: R . s c= (InvCl R) . s by PBOOLE:def_2; the Element of R . s in R . s ; hence not (InvCl R) . i is empty by A1; ::_thesis: verum end; cluster StabCl R -> V16() stable ; coherence StabCl R is non-empty proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in the carrier of S or not (StabCl R) . i is empty ) assume i in the carrier of S ; ::_thesis: not (StabCl R) . i is empty then reconsider s = i as SortSymbol of S ; set x = the Element of R . s; R c= StabCl R by Def12; then A2: R . s c= (StabCl R) . s by PBOOLE:def_2; the Element of R . s in R . s ; hence not (StabCl R) . i is empty by A2; ::_thesis: verum end; cluster TRS R -> V16() invariant stable ; coherence TRS R is non-empty proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in the carrier of S or not (TRS R) . i is empty ) assume i in the carrier of S ; ::_thesis: not (TRS R) . i is empty then reconsider s = i as SortSymbol of S ; set x = the Element of R . s; R c= TRS R by Def13; then A3: R . s c= (TRS R) . s by PBOOLE:def_2; the Element of R . s in R . s ; hence not (TRS R) . i is empty by A3; ::_thesis: verum end; end; theorem :: MSUALG_6:33 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being invariant ManySortedRelation of A holds InvCl R = R proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being invariant ManySortedRelation of A holds InvCl R = R let A be non-empty MSAlgebra over S; ::_thesis: for R being invariant ManySortedRelation of A holds InvCl R = R let R be invariant ManySortedRelation of A; ::_thesis: InvCl R = R ( InvCl R c= R & R c= InvCl R ) by Def11; hence InvCl R = R by PBOOLE:146; ::_thesis: verum end; theorem :: MSUALG_6:34 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being stable ManySortedRelation of A holds StabCl R = R proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being stable ManySortedRelation of A holds StabCl R = R let A be non-empty MSAlgebra over S; ::_thesis: for R being stable ManySortedRelation of A holds StabCl R = R let R be stable ManySortedRelation of A; ::_thesis: StabCl R = R ( StabCl R c= R & R c= StabCl R ) by Def12; hence StabCl R = R by PBOOLE:146; ::_thesis: verum end; theorem :: MSUALG_6:35 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being invariant stable ManySortedRelation of A holds TRS R = R proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being invariant stable ManySortedRelation of A holds TRS R = R let A be non-empty MSAlgebra over S; ::_thesis: for R being invariant stable ManySortedRelation of A holds TRS R = R let R be invariant stable ManySortedRelation of A; ::_thesis: TRS R = R ( TRS R c= R & R c= TRS R ) by Def13; hence TRS R = R by PBOOLE:146; ::_thesis: verum end; theorem :: MSUALG_6:36 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A holds ( StabCl R c= TRS R & InvCl R c= TRS R & StabCl (InvCl R) c= TRS R ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A holds ( StabCl R c= TRS R & InvCl R c= TRS R & StabCl (InvCl R) c= TRS R ) let A be non-empty MSAlgebra over S; ::_thesis: for R being ManySortedRelation of the Sorts of A holds ( StabCl R c= TRS R & InvCl R c= TRS R & StabCl (InvCl R) c= TRS R ) let R be ManySortedRelation of the Sorts of A; ::_thesis: ( StabCl R c= TRS R & InvCl R c= TRS R & StabCl (InvCl R) c= TRS R ) R c= TRS R by Def13; hence ( StabCl R c= TRS R & InvCl R c= TRS R ) by Def11, Def12; ::_thesis: StabCl (InvCl R) c= TRS R hence StabCl (InvCl R) c= TRS R by Def12; ::_thesis: verum end; theorem Th37: :: MSUALG_6:37 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) = TRS R proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) = TRS R let A be non-empty MSAlgebra over S; ::_thesis: for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) = TRS R let R be ManySortedRelation of the Sorts of A; ::_thesis: InvCl (StabCl R) = TRS R A1: StabCl R c= InvCl (StabCl R) by Def11; R c= TRS R by Def13; then StabCl R c= TRS R by Def12; then A2: InvCl (StabCl R) c= TRS R by Def11; A3: InvCl (StabCl R) is invariant stable ManySortedRelation of A by Th30; R c= StabCl R by Def12; then R c= InvCl (StabCl R) by A1, PBOOLE:13; then TRS R c= InvCl (StabCl R) by A3, Def13; hence InvCl (StabCl R) = TRS R by A2, PBOOLE:146; ::_thesis: verum end; theorem :: MSUALG_6:38 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st ( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st ( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) ) let A be non-empty MSAlgebra over S; ::_thesis: for R being ManySortedRelation of the Sorts of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st ( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) ) let R be ManySortedRelation of the Sorts of A; ::_thesis: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st ( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) ) let s be SortSymbol of S; ::_thesis: for a, b being Element of A,s holds ( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st ( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) ) let a, b be Element of A,s; ::_thesis: ( [a,b] in (TRS R) . s iff ex s9 being SortSymbol of S st ( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) ) A1: InvCl (StabCl R) = TRS R by Th37; hereby ::_thesis: ( ex s9 being SortSymbol of S st ( TranslationRel S reduces s9,s & ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ) implies [a,b] in (TRS R) . s ) assume [a,b] in (TRS R) . s ; ::_thesis: ex s9 being SortSymbol of S st ( TranslationRel S reduces s9,s & ex u, v being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) ) ) then consider s9 being SortSymbol of S, x, y being Element of A,s9, t being Translation of A,s9,s such that A2: TranslationRel S reduces s9,s and A3: [x,y] in (StabCl R) . s9 and A4: a = t . x and A5: b = t . y by A1, Th29; take s9 = s9; ::_thesis: ( TranslationRel S reduces s9,s & ex u, v being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) ) ) thus TranslationRel S reduces s9,s by A2; ::_thesis: ex u, v being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) ) reconsider t = t as Translation of A,s9,s ; consider u, v being Element of A,s9, h being Endomorphism of A such that A6: [u,v] in R . s9 and A7: x = (h . s9) . u and A8: y = (h . s9) . v by A3, Th31; take u = u; ::_thesis: ex v being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) ) take v = v; ::_thesis: ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) ) take h = h; ::_thesis: ex t being Translation of A,s9,s st ( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) ) take t = t; ::_thesis: ( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) ) thus ( [u,v] in R . s9 & a = t . ((h . s9) . u) & b = t . ((h . s9) . v) ) by A4, A5, A6, A7, A8; ::_thesis: verum end; given s9 being SortSymbol of S such that A9: TranslationRel S reduces s9,s and A10: ex l, r being Element of A,s9 ex h being Endomorphism of A ex t being Translation of A,s9,s st ( [l,r] in R . s9 & a = t . ((h . s9) . l) & b = t . ((h . s9) . r) ) ; ::_thesis: [a,b] in (TRS R) . s consider l, r being Element of A,s9, h being Endomorphism of A, t being Translation of A,s9,s such that A11: [l,r] in R . s9 and A12: a = t . ((h . s9) . l) and A13: b = t . ((h . s9) . r) by A10; [((h . s9) . l),((h . s9) . r)] in (StabCl R) . s9 by A11, Th31; hence [a,b] in (TRS R) . s by A1, A9, A12, A13, Th29; ::_thesis: verum end; begin theorem Th39: :: MSUALG_6:39 for A being set for R, E being Relation of A st ( for a, b being set st a in A & b in A holds ( [a,b] in E iff a,b are_convertible_wrt R ) ) holds ( E is total & E is symmetric & E is transitive ) proof let A be set ; ::_thesis: for R, E being Relation of A st ( for a, b being set st a in A & b in A holds ( [a,b] in E iff a,b are_convertible_wrt R ) ) holds ( E is total & E is symmetric & E is transitive ) let R, E be Relation of A; ::_thesis: ( ( for a, b being set st a in A & b in A holds ( [a,b] in E iff a,b are_convertible_wrt R ) ) implies ( E is total & E is symmetric & E is transitive ) ) set X = A; assume A1: for a, b being set st a in A & b in A holds ( [a,b] in E iff a,b are_convertible_wrt R ) ; ::_thesis: ( E is total & E is symmetric & E is transitive ) now__::_thesis:_for_x_being_set_st_x_in_A_holds_ [x,x]_in_E let x be set ; ::_thesis: ( x in A implies [x,x] in E ) x,x are_convertible_wrt R by REWRITE1:26; hence ( x in A implies [x,x] in E ) by A1; ::_thesis: verum end; then A2: E is_reflexive_in A by RELAT_2:def_1; then A3: field E = A by ORDERS_1:13; dom E = A by A2, ORDERS_1:13; hence E is total by PARTFUN1:def_2; ::_thesis: ( E is symmetric & E is transitive ) now__::_thesis:_for_x,_y_being_set_st_x_in_A_&_y_in_A_&_[x,y]_in_E_holds_ [y,x]_in_E let x, y be set ; ::_thesis: ( x in A & y in A & [x,y] in E implies [y,x] in E ) assume that A4: x in A and A5: y in A ; ::_thesis: ( [x,y] in E implies [y,x] in E ) assume [x,y] in E ; ::_thesis: [y,x] in E then x,y are_convertible_wrt R by A1, A4, A5; then y,x are_convertible_wrt R by REWRITE1:31; hence [y,x] in E by A1, A4, A5; ::_thesis: verum end; then E is_symmetric_in A by RELAT_2:def_3; hence E is symmetric by A3, RELAT_2:def_11; ::_thesis: E is transitive now__::_thesis:_for_x,_y,_z_being_set_st_x_in_A_&_y_in_A_&_z_in_A_&_[x,y]_in_E_&_[y,z]_in_E_holds_ [x,z]_in_E let x, y, z be set ; ::_thesis: ( x in A & y in A & z in A & [x,y] in E & [y,z] in E implies [x,z] in E ) assume that A6: x in A and A7: y in A and A8: z in A ; ::_thesis: ( [x,y] in E & [y,z] in E implies [x,z] in E ) assume that A9: [x,y] in E and A10: [y,z] in E ; ::_thesis: [x,z] in E A11: y,z are_convertible_wrt R by A1, A7, A8, A10; x,y are_convertible_wrt R by A1, A6, A7, A9; then x,z are_convertible_wrt R by A11, REWRITE1:30; hence [x,z] in E by A1, A6, A8; ::_thesis: verum end; then E is_transitive_in A by RELAT_2:def_8; hence E is transitive by A3, RELAT_2:def_16; ::_thesis: verum end; theorem Th40: :: MSUALG_6:40 for A being set for R being Relation of A for E being Equivalence_Relation of A st R c= E holds for a, b being set st a in A & a,b are_convertible_wrt R holds [a,b] in E proof let A be set ; ::_thesis: for R being Relation of A for E being Equivalence_Relation of A st R c= E holds for a, b being set st a in A & a,b are_convertible_wrt R holds [a,b] in E let R be Relation of A; ::_thesis: for E being Equivalence_Relation of A st R c= E holds for a, b being set st a in A & a,b are_convertible_wrt R holds [a,b] in E let E be Equivalence_Relation of A; ::_thesis: ( R c= E implies for a, b being set st a in A & a,b are_convertible_wrt R holds [a,b] in E ) assume A1: R c= E ; ::_thesis: for a, b being set st a in A & a,b are_convertible_wrt R holds [a,b] in E let a, b be set ; ::_thesis: ( a in A & a,b are_convertible_wrt R implies [a,b] in E ) assume A2: a in A ; ::_thesis: ( not a,b are_convertible_wrt R or [a,b] in E ) assume R \/ (R ~) reduces a,b ; :: according to REWRITE1:def_4 ::_thesis: [a,b] in E then consider p being RedSequence of R \/ (R ~) such that A3: p . 1 = a and A4: p . (len p) = b by REWRITE1:def_3; defpred S1[ Element of NAT ] means ( \$1 in dom p implies [a,(p . \$1)] in E ); A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume that A6: ( i in dom p implies [a,(p . i)] in E ) and A7: i + 1 in dom p ; ::_thesis: [a,(p . (i + 1))] in E A8: i <= i + 1 by NAT_1:11; i + 1 <= len p by A7, FINSEQ_3:25; then A9: i <= len p by A8, XXREAL_0:2; percases ( i = 0 or i > 0 ) ; suppose i = 0 ; ::_thesis: [a,(p . (i + 1))] in E hence [a,(p . (i + 1))] in E by A2, A3, EQREL_1:5; ::_thesis: verum end; suppose i > 0 ; ::_thesis: [a,(p . (i + 1))] in E then A10: i >= 0 + 1 by NAT_1:13; then i in dom p by A9, FINSEQ_3:25; then A11: [(p . i),(p . (i + 1))] in R \/ (R ~) by A7, REWRITE1:def_2; then reconsider ppi = p . i, pj = p . (i + 1) as Element of A by ZFMISC_1:87; ( [(p . i),(p . (i + 1))] in R or [(p . i),(p . (i + 1))] in R ~ ) by A11, XBOOLE_0:def_3; then ( [(p . i),(p . (i + 1))] in R or [(p . (i + 1)),(p . i)] in R ) by RELAT_1:def_7; then [ppi,pj] in E by A1, EQREL_1:6; hence [a,(p . (i + 1))] in E by A6, A9, A10, EQREL_1:7, FINSEQ_3:25; ::_thesis: verum end; end; end; A12: len p in dom p by FINSEQ_5:6; A13: S1[ 0 ] by FINSEQ_3:25; for i being Element of NAT holds S1[i] from NAT_1:sch_1(A13, A5); hence [a,b] in E by A4, A12; ::_thesis: verum end; theorem Th41: :: MSUALG_6:41 for A being non empty set for R being Relation of A for a, b being Element of A holds ( [a,b] in EqCl R iff a,b are_convertible_wrt R ) proof let A be non empty set ; ::_thesis: for R being Relation of A for a, b being Element of A holds ( [a,b] in EqCl R iff a,b are_convertible_wrt R ) let R be Relation of A; ::_thesis: for a, b being Element of A holds ( [a,b] in EqCl R iff a,b are_convertible_wrt R ) defpred S1[ set , set ] means \$1,\$2 are_convertible_wrt R; consider Q being Relation of A such that A1: for a, b being set holds ( [a,b] in Q iff ( a in A & b in A & S1[a,b] ) ) from RELSET_1:sch_1(); for a, b being set st a in A & b in A holds ( [a,b] in Q iff a,b are_convertible_wrt R ) by A1; then reconsider Q = Q as Equivalence_Relation of A by Th39; A2: now__::_thesis:_for_E_being_Equivalence_Relation_of_A_st_R_c=_E_holds_ Q_c=_E let E be Equivalence_Relation of A; ::_thesis: ( R c= E implies Q c= E ) assume A3: R c= E ; ::_thesis: Q c= E thus Q c= E ::_thesis: verum proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in Q or [x,y] in E ) assume A4: [x,y] in Q ; ::_thesis: [x,y] in E then A5: x,y are_convertible_wrt R by A1; x in A by A1, A4; hence [x,y] in E by A3, A5, Th40; ::_thesis: verum end; end; R c= Q proof let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in R or [a,b] in Q ) assume A6: [a,b] in R ; ::_thesis: [a,b] in Q then A7: b in A by ZFMISC_1:87; A8: a,b are_convertible_wrt R by A6, REWRITE1:29; a in A by A6, ZFMISC_1:87; hence [a,b] in Q by A1, A7, A8; ::_thesis: verum end; then Q = EqCl R by A2, MSUALG_5:def_1; hence for a, b being Element of A holds ( [a,b] in EqCl R iff a,b are_convertible_wrt R ) by A1; ::_thesis: verum end; theorem Th42: :: MSUALG_6:42 for S being non empty set for A being V16() ManySortedSet of S for R being ManySortedRelation of A for s being Element of S for a, b being Element of A . s holds ( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s ) proof let S be non empty set ; ::_thesis: for A being V16() ManySortedSet of S for R being ManySortedRelation of A for s being Element of S for a, b being Element of A . s holds ( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s ) let A be V16() ManySortedSet of S; ::_thesis: for R being ManySortedRelation of A for s being Element of S for a, b being Element of A . s holds ( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s ) let R be ManySortedRelation of A; ::_thesis: for s being Element of S for a, b being Element of A . s holds ( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s ) let s be Element of S; ::_thesis: for a, b being Element of A . s holds ( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s ) (EqCl R) . s = EqCl (R . s) by MSUALG_5:def_3; hence for a, b being Element of A . s holds ( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s ) by Th41; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; mode EquationalTheory of A is MSEquivalence-like invariant stable ManySortedRelation of A; let R be ManySortedRelation of A; func EqCl (R,A) -> MSEquivalence-like ManySortedRelation of A equals :: MSUALG_6:def 14 EqCl R; coherence EqCl R is MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3; end; :: deftheorem defines EqCl MSUALG_6:def_14_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of A holds EqCl (R,A) = EqCl R; theorem Th43: :: MSUALG_6:43 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of A holds R c= EqCl (R,A) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being ManySortedRelation of A holds R c= EqCl (R,A) let A be non-empty MSAlgebra over S; ::_thesis: for R being ManySortedRelation of A holds R c= EqCl (R,A) let R be ManySortedRelation of A; ::_thesis: R c= EqCl (R,A) let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or R . i c= (EqCl (R,A)) . i ) assume i in the carrier of S ; ::_thesis: R . i c= (EqCl (R,A)) . i then reconsider s = i as SortSymbol of S ; (EqCl (R,A)) . s = EqCl (R . s) by MSUALG_5:def_3; hence R . i c= (EqCl (R,A)) . i by MSUALG_5:def_1; ::_thesis: verum end; theorem Th44: :: MSUALG_6:44 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of A for E being MSEquivalence-like ManySortedRelation of A st R c= E holds EqCl (R,A) c= E proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being ManySortedRelation of A for E being MSEquivalence-like ManySortedRelation of A st R c= E holds EqCl (R,A) c= E let A be non-empty MSAlgebra over S; ::_thesis: for R being ManySortedRelation of A for E being MSEquivalence-like ManySortedRelation of A st R c= E holds EqCl (R,A) c= E let R be ManySortedRelation of A; ::_thesis: for E being MSEquivalence-like ManySortedRelation of A st R c= E holds EqCl (R,A) c= E let E be MSEquivalence-like ManySortedRelation of A; ::_thesis: ( R c= E implies EqCl (R,A) c= E ) assume A1: R c= E ; ::_thesis: EqCl (R,A) c= E let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or (EqCl (R,A)) . i c= E . i ) assume i in the carrier of S ; ::_thesis: (EqCl (R,A)) . i c= E . i then reconsider s = i as SortSymbol of S ; A2: (EqCl (R,A)) . s = EqCl (R . s) by MSUALG_5:def_3; R . s c= E . s by A1, PBOOLE:def_2; hence (EqCl (R,A)) . i c= E . i by A2, MSUALG_5:def_1; ::_thesis: verum end; theorem Th45: :: MSUALG_6:45 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being stable ManySortedRelation of A for s being SortSymbol of S for a, b being Element of A,s st a,b are_convertible_wrt R . s holds for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being stable ManySortedRelation of A for s being SortSymbol of S for a, b being Element of A,s st a,b are_convertible_wrt R . s holds for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s let A be non-empty MSAlgebra over S; ::_thesis: for R being stable ManySortedRelation of A for s being SortSymbol of S for a, b being Element of A,s st a,b are_convertible_wrt R . s holds for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s let R be stable ManySortedRelation of A; ::_thesis: for s being SortSymbol of S for a, b being Element of A,s st a,b are_convertible_wrt R . s holds for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s let s be SortSymbol of S; ::_thesis: for a, b being Element of A,s st a,b are_convertible_wrt R . s holds for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s let a, b be Element of A,s; ::_thesis: ( a,b are_convertible_wrt R . s implies for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s ) assume (R . s) \/ ((R . s) ~) reduces a,b ; :: according to REWRITE1:def_4 ::_thesis: for h being Endomorphism of A holds (h . s) . a,(h . s) . b are_convertible_wrt R . s then consider p being RedSequence of (R . s) \/ ((R . s) ~) such that A1: p . 1 = a and A2: p . (len p) = b by REWRITE1:def_3; let h be Endomorphism of A; ::_thesis: (h . s) . a,(h . s) . b are_convertible_wrt R . s defpred S1[ Element of NAT ] means ( \$1 in dom p implies (h . s) . a,(h . s) . (p . \$1) are_convertible_wrt R . s ); A3: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume that A4: ( i in dom p implies (h . s) . a,(h . s) . (p . i) are_convertible_wrt R . s ) and A5: i + 1 in dom p ; ::_thesis: (h . s) . a,(h . s) . (p . (i + 1)) are_convertible_wrt R . s A6: i <= i + 1 by NAT_1:11; i + 1 <= len p by A5, FINSEQ_3:25; then A7: i <= len p by A6, XXREAL_0:2; percases ( i = 0 or i > 0 ) ; suppose i = 0 ; ::_thesis: (h . s) . a,(h . s) . (p . (i + 1)) are_convertible_wrt R . s hence (h . s) . a,(h . s) . (p . (i + 1)) are_convertible_wrt R . s by A1, REWRITE1:26; ::_thesis: verum end; suppose i > 0 ; ::_thesis: (h . s) . a,(h . s) . (p . (i + 1)) are_convertible_wrt R . s then A8: i >= 0 + 1 by NAT_1:13; then i in dom p by A7, FINSEQ_3:25; then A9: [(p . i),(p . (i + 1))] in (R . s) \/ ((R . s) ~) by A5, REWRITE1:def_2; then reconsider ppi = p . i, pj = p . (i + 1) as Element of A,s by ZFMISC_1:87; ( [(p . i),(p . (i + 1))] in R . s or [(p . i),(p . (i + 1))] in (R . s) ~ ) by A9, XBOOLE_0:def_3; then ( [(p . i),(p . (i + 1))] in R . s or [(p . (i + 1)),(p . i)] in R . s ) by RELAT_1:def_7; then ( [((h . s) . ppi),((h . s) . pj)] in R . s or [((h . s) . pj),((h . s) . ppi)] in R . s ) by Def9; then ( (h . s) . ppi,(h . s) . pj are_convertible_wrt R . s or (h . s) . pj,(h . s) . ppi are_convertible_wrt R . s ) by REWRITE1:29; then (h . s) . ppi,(h . s) . pj are_convertible_wrt R . s by REWRITE1:31; hence (h . s) . a,(h . s) . (p . (i + 1)) are_convertible_wrt R . s by A4, A7, A8, FINSEQ_3:25, REWRITE1:30; ::_thesis: verum end; end; end; A10: len p in dom p by FINSEQ_5:6; A11: S1[ 0 ] by FINSEQ_3:25; for i being Element of NAT holds S1[i] from NAT_1:sch_1(A11, A3); hence (h . s) . a,(h . s) . b are_convertible_wrt R . s by A2, A10; ::_thesis: verum end; theorem Th46: :: MSUALG_6:46 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being stable ManySortedRelation of A holds EqCl (R,A) is stable proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being stable ManySortedRelation of A holds EqCl (R,A) is stable let A be non-empty MSAlgebra over S; ::_thesis: for R being stable ManySortedRelation of A holds EqCl (R,A) is stable let R be stable ManySortedRelation of A; ::_thesis: EqCl (R,A) is stable let h be Endomorphism of A; :: according to MSUALG_6:def_9 ::_thesis: for s being SortSymbol of S for a, b being set st [a,b] in (EqCl (R,A)) . s holds [((h . s) . a),((h . s) . b)] in (EqCl (R,A)) . s let s be SortSymbol of S; ::_thesis: for a, b being set st [a,b] in (EqCl (R,A)) . s holds [((h . s) . a),((h . s) . b)] in (EqCl (R,A)) . s let a, b be set ; ::_thesis: ( [a,b] in (EqCl (R,A)) . s implies [((h . s) . a),((h . s) . b)] in (EqCl (R,A)) . s ) assume A1: [a,b] in (EqCl (R,A)) . s ; ::_thesis: [((h . s) . a),((h . s) . b)] in (EqCl (R,A)) . s then reconsider a = a, b = b as Element of A,s by ZFMISC_1:87; a,b are_convertible_wrt R . s by A1, Th42; then (h . s) . a,(h . s) . b are_convertible_wrt R . s by Th45; hence [((h . s) . a),((h . s) . b)] in (EqCl (R,A)) . s by Th42; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let R be stable ManySortedRelation of A; cluster EqCl (R,A) -> MSEquivalence-like stable ; coherence EqCl (R,A) is stable by Th46; end; theorem Th47: :: MSUALG_6:47 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being invariant ManySortedRelation of A for s1, s2 being SortSymbol of S for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds for t being Function st t is_e.translation_of A,s1,s2 holds t . a,t . b are_convertible_wrt R . s2 proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being invariant ManySortedRelation of A for s1, s2 being SortSymbol of S for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds for t being Function st t is_e.translation_of A,s1,s2 holds t . a,t . b are_convertible_wrt R . s2 let A be non-empty MSAlgebra over S; ::_thesis: for R being invariant ManySortedRelation of A for s1, s2 being SortSymbol of S for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds for t being Function st t is_e.translation_of A,s1,s2 holds t . a,t . b are_convertible_wrt R . s2 let R be invariant ManySortedRelation of A; ::_thesis: for s1, s2 being SortSymbol of S for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds for t being Function st t is_e.translation_of A,s1,s2 holds t . a,t . b are_convertible_wrt R . s2 let s1, s2 be SortSymbol of S; ::_thesis: for a, b being Element of A,s1 st a,b are_convertible_wrt R . s1 holds for t being Function st t is_e.translation_of A,s1,s2 holds t . a,t . b are_convertible_wrt R . s2 let a, b be Element of A,s1; ::_thesis: ( a,b are_convertible_wrt R . s1 implies for t being Function st t is_e.translation_of A,s1,s2 holds t . a,t . b are_convertible_wrt R . s2 ) assume (R . s1) \/ ((R . s1) ~) reduces a,b ; :: according to REWRITE1:def_4 ::_thesis: for t being Function st t is_e.translation_of A,s1,s2 holds t . a,t . b are_convertible_wrt R . s2 then consider p being RedSequence of (R . s1) \/ ((R . s1) ~) such that A1: p . 1 = a and A2: p . (len p) = b by REWRITE1:def_3; let t be Function; ::_thesis: ( t is_e.translation_of A,s1,s2 implies t . a,t . b are_convertible_wrt R . s2 ) assume A3: t is_e.translation_of A,s1,s2 ; ::_thesis: t . a,t . b are_convertible_wrt R . s2 defpred S1[ Element of NAT ] means ( \$1 in dom p implies t . a,t . (p . \$1) are_convertible_wrt R . s2 ); A4: for i being Element of NAT st S1[i] holds S1[i + 1] proof let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume that A5: ( i in dom p implies t . a,t . (p . i) are_convertible_wrt R . s2 ) and A6: i + 1 in dom p ; ::_thesis: t . a,t . (p . (i + 1)) are_convertible_wrt R . s2 A7: i <= i + 1 by NAT_1:11; i + 1 <= len p by A6, FINSEQ_3:25; then A8: i <= len p by A7, XXREAL_0:2; percases ( i = 0 or i > 0 ) ; suppose i = 0 ; ::_thesis: t . a,t . (p . (i + 1)) are_convertible_wrt R . s2 hence t . a,t . (p . (i + 1)) are_convertible_wrt R . s2 by A1, REWRITE1:26; ::_thesis: verum end; suppose i > 0 ; ::_thesis: t . a,t . (p . (i + 1)) are_convertible_wrt R . s2 then A9: i >= 0 + 1 by NAT_1:13; then i in dom p by A8, FINSEQ_3:25; then A10: [(p . i),(p . (i + 1))] in (R . s1) \/ ((R . s1) ~) by A6, REWRITE1:def_2; then reconsider ppi = p . i, pj = p . (i + 1) as Element of A,s1 by ZFMISC_1:87; ( [(p . i),(p . (i + 1))] in R . s1 or [(p . i),(p . (i + 1))] in (R . s1) ~ ) by A10, XBOOLE_0:def_3; then ( [(p . i),(p . (i + 1))] in R . s1 or [(p . (i + 1)),(p . i)] in R . s1 ) by RELAT_1:def_7; then ( [(t . ppi),(t . pj)] in R . s2 or [(t . pj),(t . ppi)] in R . s2 ) by A3, Def8; then ( t . ppi,t . pj are_convertible_wrt R . s2 or t . pj,t . ppi are_convertible_wrt R . s2 ) by REWRITE1:29; then t . ppi,t . pj are_convertible_wrt R . s2 by REWRITE1:31; hence t . a,t . (p . (i + 1)) are_convertible_wrt R . s2 by A5, A8, A9, FINSEQ_3:25, REWRITE1:30; ::_thesis: verum end; end; end; A11: len p in dom p by FINSEQ_5:6; A12: S1[ 0 ] by FINSEQ_3:25; for i being Element of NAT holds S1[i] from NAT_1:sch_1(A12, A4); hence t . a,t . b are_convertible_wrt R . s2 by A2, A11; ::_thesis: verum end; theorem Th48: :: MSUALG_6:48 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being invariant ManySortedRelation of A holds EqCl (R,A) is invariant proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being invariant ManySortedRelation of A holds EqCl (R,A) is invariant let A be non-empty MSAlgebra over S; ::_thesis: for R being invariant ManySortedRelation of A holds EqCl (R,A) is invariant let R be invariant ManySortedRelation of A; ::_thesis: EqCl (R,A) is invariant let s1, s2 be SortSymbol of S; :: according to MSUALG_6:def_8 ::_thesis: for t being Function st t is_e.translation_of A,s1,s2 holds for a, b being set st [a,b] in (EqCl (R,A)) . s1 holds [(t . a),(t . b)] in (EqCl (R,A)) . s2 let t be Function; ::_thesis: ( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in (EqCl (R,A)) . s1 holds [(t . a),(t . b)] in (EqCl (R,A)) . s2 ) assume A1: t is_e.translation_of A,s1,s2 ; ::_thesis: for a, b being set st [a,b] in (EqCl (R,A)) . s1 holds [(t . a),(t . b)] in (EqCl (R,A)) . s2 then reconsider t = t as Function of ( the Sorts of A . s1),( the Sorts of A . s2) by Th11; let a, b be set ; ::_thesis: ( [a,b] in (EqCl (R,A)) . s1 implies [(t . a),(t . b)] in (EqCl (R,A)) . s2 ) assume A2: [a,b] in (EqCl (R,A)) . s1 ; ::_thesis: [(t . a),(t . b)] in (EqCl (R,A)) . s2 then reconsider a = a, b = b as Element of A,s1 by ZFMISC_1:87; a,b are_convertible_wrt R . s1 by A2, Th42; then t . a,t . b are_convertible_wrt R . s2 by A1, Th47; hence [(t . a),(t . b)] in (EqCl (R,A)) . s2 by Th42; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let R be invariant ManySortedRelation of A; cluster EqCl (R,A) -> MSEquivalence-like invariant ; coherence EqCl (R,A) is invariant by Th48; end; theorem Th49: :: MSUALG_6:49 for S being non empty set for A being V16() ManySortedSet of S for R, E being ManySortedRelation of A st ( for s being Element of S for a, b being Element of A . s holds ( [a,b] in E . s iff a,b are_convertible_wrt R . s ) ) holds E is MSEquivalence_Relation-like proof let S be non empty set ; ::_thesis: for A being V16() ManySortedSet of S for R, E being ManySortedRelation of A st ( for s being Element of S for a, b being Element of A . s holds ( [a,b] in E . s iff a,b are_convertible_wrt R . s ) ) holds E is MSEquivalence_Relation-like let A be V16() ManySortedSet of S; ::_thesis: for R, E being ManySortedRelation of A st ( for s being Element of S for a, b being Element of A . s holds ( [a,b] in E . s iff a,b are_convertible_wrt R . s ) ) holds E is MSEquivalence_Relation-like let R, E be ManySortedRelation of A; ::_thesis: ( ( for s being Element of S for a, b being Element of A . s holds ( [a,b] in E . s iff a,b are_convertible_wrt R . s ) ) implies E is MSEquivalence_Relation-like ) assume A1: for s being Element of S for a, b being Element of A . s holds ( [a,b] in E . s iff a,b are_convertible_wrt R . s ) ; ::_thesis: E is MSEquivalence_Relation-like let i be set ; :: according to MSUALG_4:def_2 ::_thesis: for b1 being Element of bool [:(A . i),(A . i):] holds ( not i in S or not E . i = b1 or b1 is Element of bool [:(A . i),(A . i):] ) let P be Relation of (A . i); ::_thesis: ( not i in S or not E . i = P or P is Element of bool [:(A . i),(A . i):] ) assume i in S ; ::_thesis: ( not E . i = P or P is Element of bool [:(A . i),(A . i):] ) then reconsider s = i as Element of S ; for a, b being set st a in A . s & b in A . s holds ( [a,b] in E . s iff a,b are_convertible_wrt R . s ) by A1; hence ( not E . i = P or P is Element of bool [:(A . i),(A . i):] ) by Th39; ::_thesis: verum end; theorem Th50: :: MSUALG_6:50 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R, E being ManySortedRelation of A st ( for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ) holds E is EquationalTheory of A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R, E being ManySortedRelation of A st ( for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ) holds E is EquationalTheory of A let A be non-empty MSAlgebra over S; ::_thesis: for R, E being ManySortedRelation of A st ( for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ) holds E is EquationalTheory of A let R, E be ManySortedRelation of A; ::_thesis: ( ( for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ) implies E is EquationalTheory of A ) assume A1: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in E . s iff a,b are_convertible_wrt (TRS R) . s ) ; ::_thesis: E is EquationalTheory of A A2: E is stable proof let h be Endomorphism of A; :: according to MSUALG_6:def_9 ::_thesis: for s being SortSymbol of S for a, b being set st [a,b] in E . s holds [((h . s) . a),((h . s) . b)] in E . s let s be SortSymbol of S; ::_thesis: for a, b being set st [a,b] in E . s holds [((h . s) . a),((h . s) . b)] in E . s let a, b be set ; ::_thesis: ( [a,b] in E . s implies [((h . s) . a),((h . s) . b)] in E . s ) assume A3: [a,b] in E . s ; ::_thesis: [((h . s) . a),((h . s) . b)] in E . s then reconsider x = a, y = b as Element of A,s by ZFMISC_1:87; reconsider a9 = (h . s) . x, b9 = (h . s) . y as Element of A,s ; x,y are_convertible_wrt (TRS R) . s by A1, A3; then a9,b9 are_convertible_wrt (TRS R) . s by Th45; hence [((h . s) . a),((h . s) . b)] in E . s by A1; ::_thesis: verum end; A4: E is invariant proof let s1, s2 be SortSymbol of S; :: according to MSUALG_6:def_8 ::_thesis: for t being Function st t is_e.translation_of A,s1,s2 holds for a, b being set st [a,b] in E . s1 holds [(t . a),(t . b)] in E . s2 let t be Function; ::_thesis: ( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in E . s1 holds [(t . a),(t . b)] in E . s2 ) assume A5: t is_e.translation_of A,s1,s2 ; ::_thesis: for a, b being set st [a,b] in E . s1 holds [(t . a),(t . b)] in E . s2 then reconsider f = t as Function of ( the Sorts of A . s1),( the Sorts of A . s2) by Th11; let a, b be set ; ::_thesis: ( [a,b] in E . s1 implies [(t . a),(t . b)] in E . s2 ) assume A6: [a,b] in E . s1 ; ::_thesis: [(t . a),(t . b)] in E . s2 then reconsider x = a, y = b as Element of A,s1 by ZFMISC_1:87; x,y are_convertible_wrt (TRS R) . s1 by A1, A6; then A7: t . x,t . y are_convertible_wrt (TRS R) . s2 by A5, Th47; A8: t . y = f . y ; t . x = f . x ; hence [(t . a),(t . b)] in E . s2 by A1, A8, A7; ::_thesis: verum end; E is MSEquivalence_Relation-like by A1, Th49; hence E is EquationalTheory of A by A2, A4, MSUALG_4:def_3; ::_thesis: verum end; theorem Th51: :: MSUALG_6:51 for S being non empty set for A being V16() ManySortedSet of S for R being ManySortedRelation of A for E being MSEquivalence_Relation-like ManySortedRelation of A st R c= E holds for s being Element of S for a, b being Element of A . s st a,b are_convertible_wrt R . s holds [a,b] in E . s proof let S be non empty set ; ::_thesis: for A being V16() ManySortedSet of S for R being ManySortedRelation of A for E being MSEquivalence_Relation-like ManySortedRelation of A st R c= E holds for s being Element of S for a, b being Element of A . s st a,b are_convertible_wrt R . s holds [a,b] in E . s let A be V16() ManySortedSet of S; ::_thesis: for R being ManySortedRelation of A for E being MSEquivalence_Relation-like ManySortedRelation of A st R c= E holds for s being Element of S for a, b being Element of A . s st a,b are_convertible_wrt R . s holds [a,b] in E . s let R be ManySortedRelation of A; ::_thesis: for E being MSEquivalence_Relation-like ManySortedRelation of A st R c= E holds for s being Element of S for a, b being Element of A . s st a,b are_convertible_wrt R . s holds [a,b] in E . s let E be MSEquivalence_Relation-like ManySortedRelation of A; ::_thesis: ( R c= E implies for s being Element of S for a, b being Element of A . s st a,b are_convertible_wrt R . s holds [a,b] in E . s ) assume A1: R c= E ; ::_thesis: for s being Element of S for a, b being Element of A . s st a,b are_convertible_wrt R . s holds [a,b] in E . s let s be Element of S; ::_thesis: for a, b being Element of A . s st a,b are_convertible_wrt R . s holds [a,b] in E . s A2: E . s is Equivalence_Relation of (A . s) by MSUALG_4:def_2; R . s c= E . s by A1, PBOOLE:def_2; hence for a, b being Element of A . s st a,b are_convertible_wrt R . s holds [a,b] in E . s by A2, Th40; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let R be ManySortedRelation of the Sorts of A; func EqTh R -> EquationalTheory of A means :Def15: :: MSUALG_6:def 15 ( R c= it & ( for Q being EquationalTheory of A st R c= Q holds it c= Q ) ); uniqueness for b1, b2 being EquationalTheory of A st R c= b1 & ( for Q being EquationalTheory of A st R c= Q holds b1 c= Q ) & R c= b2 & ( for Q being EquationalTheory of A st R c= Q holds b2 c= Q ) holds b1 = b2 proof let Q1, Q2 be EquationalTheory of A; ::_thesis: ( R c= Q1 & ( for Q being EquationalTheory of A st R c= Q holds Q1 c= Q ) & R c= Q2 & ( for Q being EquationalTheory of A st R c= Q holds Q2 c= Q ) implies Q1 = Q2 ) assume that A1: R c= Q1 and A2: for Q being EquationalTheory of A st R c= Q holds Q1 c= Q and A3: R c= Q2 and A4: for Q being EquationalTheory of A st R c= Q holds Q2 c= Q ; ::_thesis: Q1 = Q2 ( Q1 c= Q2 & Q2 c= Q1 ) by A1, A2, A3, A4; hence Q1 = Q2 by PBOOLE:146; ::_thesis: verum end; existence ex b1 being EquationalTheory of A st ( R c= b1 & ( for Q being EquationalTheory of A st R c= Q holds b1 c= Q ) ) proof defpred S1[ SortSymbol of S, set , set ] means \$2,\$3 are_convertible_wrt (TRS R) . \$1; consider P being ManySortedRelation of the Sorts of A such that A5: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in P . s iff S1[s,a,b] ) from MSUALG_6:sch_2(); reconsider P = P as ManySortedRelation of A ; reconsider P = P as EquationalTheory of A by A5, Th50; take P ; ::_thesis: ( R c= P & ( for Q being EquationalTheory of A st R c= Q holds P c= Q ) ) thus R c= P ::_thesis: for Q being EquationalTheory of A st R c= Q holds P c= Q proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or R . i c= P . i ) assume i in the carrier of S ; ::_thesis: R . i c= P . i then reconsider s = i as SortSymbol of S ; R . s c= P . s proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in R . s or [x,y] in P . s ) assume A6: [x,y] in R . s ; ::_thesis: [x,y] in P . s then reconsider a = x, b = y as Element of A,s by ZFMISC_1:87; R c= TRS R by Def13; then R . s c= (TRS R) . s by PBOOLE:def_2; then a,b are_convertible_wrt (TRS R) . s by A6, REWRITE1:29; hence [x,y] in P . s by A5; ::_thesis: verum end; hence R . i c= P . i ; ::_thesis: verum end; let Q be EquationalTheory of A; ::_thesis: ( R c= Q implies P c= Q ) assume A7: R c= Q ; ::_thesis: P c= Q let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or P . i c= Q . i ) assume i in the carrier of S ; ::_thesis: P . i c= Q . i then reconsider s = i as SortSymbol of S ; A8: TRS R c= Q by A7, Def13; P . s c= Q . s proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in P . s or [x,y] in Q . s ) assume A9: [x,y] in P . s ; ::_thesis: [x,y] in Q . s then reconsider a = x, b = y as Element of A,s by ZFMISC_1:87; a,b are_convertible_wrt (TRS R) . s by A5, A9; hence [x,y] in Q . s by A8, Th51; ::_thesis: verum end; hence P . i c= Q . i ; ::_thesis: verum end; end; :: deftheorem Def15 defines EqTh MSUALG_6:def_15_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of the Sorts of A for b4 being EquationalTheory of A holds ( b4 = EqTh R iff ( R c= b4 & ( for Q being EquationalTheory of A st R c= Q holds b4 c= Q ) ) ); theorem :: MSUALG_6:52 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of A holds ( EqCl (R,A) c= EqTh R & InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being ManySortedRelation of A holds ( EqCl (R,A) c= EqTh R & InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R ) let A be non-empty MSAlgebra over S; ::_thesis: for R being ManySortedRelation of A holds ( EqCl (R,A) c= EqTh R & InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R ) let R be ManySortedRelation of A; ::_thesis: ( EqCl (R,A) c= EqTh R & InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R ) A1: R c= EqTh R by Def15; hence EqCl (R,A) c= EqTh R by Th44; ::_thesis: ( InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R ) thus ( InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R ) by A1, Def11, Def12, Def13; ::_thesis: verum end; theorem :: MSUALG_6:53 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (EqTh R) . s iff a,b are_convertible_wrt (TRS R) . s ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being ManySortedRelation of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (EqTh R) . s iff a,b are_convertible_wrt (TRS R) . s ) let A be non-empty MSAlgebra over S; ::_thesis: for R being ManySortedRelation of A for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (EqTh R) . s iff a,b are_convertible_wrt (TRS R) . s ) let R be ManySortedRelation of A; ::_thesis: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in (EqTh R) . s iff a,b are_convertible_wrt (TRS R) . s ) let s be SortSymbol of S; ::_thesis: for a, b being Element of A,s holds ( [a,b] in (EqTh R) . s iff a,b are_convertible_wrt (TRS R) . s ) let a, b be Element of A,s; ::_thesis: ( [a,b] in (EqTh R) . s iff a,b are_convertible_wrt (TRS R) . s ) defpred S1[ SortSymbol of S, set , set ] means \$2,\$3 are_convertible_wrt (TRS R) . \$1; consider P being ManySortedRelation of the Sorts of A such that A1: for s being SortSymbol of S for a, b being Element of A,s holds ( [a,b] in P . s iff S1[s,a,b] ) from MSUALG_6:sch_2(); reconsider P = P as ManySortedRelation of A ; reconsider P = P as EquationalTheory of A by A1, Th50; R c= P proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or R . i c= P . i ) assume i in the carrier of S ; ::_thesis: R . i c= P . i then reconsider s = i as SortSymbol of S ; R . s c= P . s proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in R . s or [x,y] in P . s ) assume A2: [x,y] in R . s ; ::_thesis: [x,y] in P . s then reconsider a = x, b = y as Element of A,s by ZFMISC_1:87; R c= TRS R by Def13; then R . s c= (TRS R) . s by PBOOLE:def_2; then a,b are_convertible_wrt (TRS R) . s by A2, REWRITE1:29; hence [x,y] in P . s by A1; ::_thesis: verum end; hence R . i c= P . i ; ::_thesis: verum end; then EqTh R c= P by Def15; then (EqTh R) . s c= P . s by PBOOLE:def_2; hence ( [a,b] in (EqTh R) . s implies a,b are_convertible_wrt (TRS R) . s ) by A1; ::_thesis: ( a,b are_convertible_wrt (TRS R) . s implies [a,b] in (EqTh R) . s ) R c= EqTh R by Def15; then TRS R c= EqTh R by Def13; hence ( a,b are_convertible_wrt (TRS R) . s implies [a,b] in (EqTh R) . s ) by Th51; ::_thesis: verum end; theorem :: MSUALG_6:54 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for R being ManySortedRelation of A holds EqTh R = EqCl ((TRS R),A) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for R being ManySortedRelation of A holds EqTh R = EqCl ((TRS R),A) let A be non-empty MSAlgebra over S; ::_thesis: for R being ManySortedRelation of A holds EqTh R = EqCl ((TRS R),A) let R be ManySortedRelation of A; ::_thesis: EqTh R = EqCl ((TRS R),A) A1: TRS R c= EqCl ((TRS R),A) by Th43; R c= TRS R by Def13; then R c= EqCl ((TRS R),A) by A1, PBOOLE:13; then A2: EqTh R c= EqCl ((TRS R),A) by Def15; R c= EqTh R by Def15; then TRS R c= EqTh R by Def13; then EqCl ((TRS R),A) c= EqTh R by Th44; hence EqTh R = EqCl ((TRS R),A) by A2, PBOOLE:146; ::_thesis: verum end;