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