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 S₁[ 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 S₁[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 object ; :: 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 object ; :: 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 ;
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 ;
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