let S be locally_directed OrderSortedSign; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
let R be ManySortedRelation of (ParsedTermsOSA X); :: thesis:
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set D = DTConOSA X;
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
set C = bool [:(TS (DTConOSA X)), the carrier of S:];
set F = PTClasses X;
defpred S₁[ ManySortedSet of the carrier of S] means for s1, s2 being Element of S
for x being object st x in X . s1 holds
( ( s1 <= s2 implies [(root-tree [x,s1]),(root-tree [x,s1])] in $1 . s2 ) & ( for y being object st ( [(root-tree [x,s1]),y] in $1 . s2 or [y,(root-tree [x,s1])] in $1 . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] ) ) );
defpred S₂[ ManySortedSet of the carrier of S] means for o1, o2 being OperSymbol of S
for x1 being Element of Args (o1,(ParsedTermsOSA X))
for x2 being Element of Args (o2,(ParsedTermsOSA X))
for s3 being Element of S holds
( [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in $1 . s3 iff ( o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 & ex w3 being Element of the carrier of S * st
( dom w3 = dom x1 & ( for y being Nat st y in dom w3 holds
[(x1 . y),(x2 . y)] in $1 . (w3 /. y) ) ) ) );
set P = PTCongruence X;
A1: for R1, R2 being ManySortedRelation of (ParsedTermsOSA X) st S₁[R1] & S₂[R1] & S₁[R2] & S₂[R2] holds
R1 = R2

proof

let R1, R2 be ManySortedRelation of (ParsedTermsOSA X); :: thesis:
assume that
A2: S₁[R1] and
A3: S₂[R1] and
A4: S₁[R2] and
A5: S₂[R2] ; :: thesis:
defpred S₃[ set ] means for x being object
for s being Element of S holds
( [$1,x] in R1 . s iff [$1,x] in R2 . s );
A6: for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S₃[t] ) holds
S₃[nt -tree ts]

proof

let nt be Symbol of (DTConOSA X); :: thesis:
let ts be FinSequence of TS (DTConOSA X); :: thesis:
assume that
A7: nt ==> roots ts and
A8: for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S₃[t] ; :: thesis:
nt in { s where s is Symbol of (DTConOSA X) : ex n being FinSequence st s ==> n } by A7;
then reconsider nt1 = nt as NonTerminal of (DTConOSA X) by LANG1:def 3;
reconsider tss = ts as SubtreeSeq of nt1 by A7, DTCONSTR:def 6;
let x be object ; :: thesis:
let s be Element of S; :: thesis:
A9: rng ts c= TS (DTConOSA X) by FINSEQ_1:def 4;
[nt,(roots ts)] in the Rules of (DTConOSA X) by A7, LANG1:def 1;
then reconsider rt = roots ts as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
reconsider sy = nt as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;
[sy,rt] in OSREL X by A7, LANG1:def 1;
then sy in [: the carrier' of S,{ the carrier of S}:] by Def4;
then consider o being Element of the carrier' of S, x2 being Element of { the carrier of S} such that
A10: sy = [o,x2] by DOMAIN_1:1;
A11: x2 = the carrier of S by TARSKI:def 1;
then A12: (nt -tree tss) . {} = [o, the carrier of S] by A10, TREES_4:def 4;
then consider ts2 being SubtreeSeq of OSSym (o,X) such that
A13: nt1 -tree tss = (OSSym (o,X)) -tree ts2 and
OSSym (o,X) ==> roots ts2 and
A14: ts2 in Args (o,(ParsedTermsOSA X)) and
A15: nt1 -tree tss = (Den (o,(ParsedTermsOSA X))) . ts2 by Th11;
A16: the Sorts of (ParsedTermsOSA X) . s = ParsedTerms (X,s) by Def8
.= { a1 where a1 is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a1 . {} & the_result_sort_of o <= s ) ) } ;

hereby :: thesis:

assume A17: [(nt -tree ts),x] in R1 . s ; :: thesis:
then x in the Sorts of (ParsedTermsOSA X) . s by ZFMISC_1:87;
then consider a1 being Element of TS (DTConOSA X) such that
A18: x = a1 and
A19: ( ex s1 being Element of S ex y being object st
( s1 <= s & y in X . s1 & a1 = root-tree [y,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a1 . {} & the_result_sort_of o <= s ) ) by A16;
for s1 being Element of S
for y being set holds
( not s1 <= s or not y in X . s1 or not a1 = root-tree [y,s1] )

proof

given s1 being Element of S, y being set such that s1 <= s and
A20: y in X . s1 and
A21: a1 = root-tree [y,s1] ; :: thesis:
nt -tree ts = root-tree [y,s1] by A2, A17, A18, A20, A21;
then [y,s1] = nt by TREES_4:17;
then the carrier of S = s1 by A10, A11, XTUPLE_0:1;
then s1 in s1 ;
hence contradiction ; :: thesis:

end;

then consider o1 being OperSymbol of S such that
A22: [o1, the carrier of S] = a1 . {} and
the_result_sort_of o1 <= s by A19;
consider ts1 being SubtreeSeq of OSSym (o1,X) such that
a1 = (OSSym (o1,X)) -tree ts1 and
OSSym (o1,X) ==> roots ts1 and
A23: ts1 in Args (o1,(ParsedTermsOSA X)) and
A24: a1 = (Den (o1,(ParsedTermsOSA X))) . ts1 by A22, Th11;
consider ts2 being SubtreeSeq of OSSym (o,X) such that
A25: nt1 -tree tss = (OSSym (o,X)) -tree ts2 and
OSSym (o,X) ==> roots ts2 and
A26: ts2 in Args (o,(ParsedTermsOSA X)) and
A27: nt1 -tree tss = (Den (o,(ParsedTermsOSA X))) . ts2 by A12, Th11;
A28: len (the_arity_of o) = len (the_arity_of o1) by A3, A17, A18, A23, A24, A26, A27;
reconsider tsb = ts2 as Element of Args (o,(ParsedTermsOSA X)) by A26;
reconsider tsa = ts1 as Element of Args (o1,(ParsedTermsOSA X)) by A23;
consider w3 being Element of the carrier of S * such that
A29: dom w3 = dom tsb and
A30: for y being Nat st y in dom w3 holds
[(tsb . y),(tsa . y)] in R1 . (w3 /. y) by A3, A17, A18, A24, A27;
A31: ts2 = tss by A25, TREES_4:15;
A32: for y being Nat st y in dom w3 holds
[(tsb . y),(tsa . y)] in R2 . (w3 /. y)

proof

let y be Nat; :: thesis:
assume A33: y in dom w3 ; :: thesis:
A34: tsb . y in rng ts by A31, A29, A33, FUNCT_1:3;
then reconsider t = tsb . y as Element of TS (DTConOSA X) by A9;
[t,(tsa . y)] in R1 . (w3 /. y) by A30, A33;
hence [(tsb . y),(tsa . y)] in R2 . (w3 /. y) by A8, A34; :: thesis:

end;

A35: the_result_sort_of o1 <= s by A3, A17, A18, A23, A24, A26, A27;
A36: the_result_sort_of o <= s by A3, A17, A18, A23, A24, A26, A27;
o ~= o1 by A3, A17, A18, A23, A24, A26, A27;
hence [(nt -tree ts),x] in R2 . s by A5, A18, A24, A27, A28, A36, A35, A29, A32; :: thesis:

end;

reconsider tsb = ts2 as Element of Args (o,(ParsedTermsOSA X)) by A14;
assume A37: [(nt -tree ts),x] in R2 . s ; :: thesis:
then x in the Sorts of (ParsedTermsOSA X) . s by ZFMISC_1:87;
then consider a1 being Element of TS (DTConOSA X) such that
A38: x = a1 and
A39: ( ex s1 being Element of S ex y being object st
( s1 <= s & y in X . s1 & a1 = root-tree [y,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a1 . {} & the_result_sort_of o <= s ) ) by A16;
for s1 being Element of S
for y being set holds
( not s1 <= s or not y in X . s1 or not a1 = root-tree [y,s1] )

proof

given s1 being Element of S, y being set such that s1 <= s and
A40: y in X . s1 and
A41: a1 = root-tree [y,s1] ; :: thesis:
nt -tree ts = root-tree [y,s1] by A4, A37, A38, A40, A41;
then [y,s1] = nt by TREES_4:17;
then the carrier of S = s1 by A10, A11, XTUPLE_0:1;
then s1 in s1 ;
hence contradiction ; :: thesis:

end;

then consider o1 being OperSymbol of S such that
A42: [o1, the carrier of S] = a1 . {} and
the_result_sort_of o1 <= s by A39;
consider ts1 being SubtreeSeq of OSSym (o1,X) such that
a1 = (OSSym (o1,X)) -tree ts1 and
OSSym (o1,X) ==> roots ts1 and
A43: ts1 in Args (o1,(ParsedTermsOSA X)) and
A44: a1 = (Den (o1,(ParsedTermsOSA X))) . ts1 by A42, Th11;
A45: len (the_arity_of o) = len (the_arity_of o1) by A5, A37, A38, A43, A44, A14, A15;
reconsider tsa = ts1 as Element of Args (o1,(ParsedTermsOSA X)) by A43;
consider w3 being Element of the carrier of S * such that
A46: dom w3 = dom tsb and
A47: for y being Nat st y in dom w3 holds
[(tsb . y),(tsa . y)] in R2 . (w3 /. y) by A5, A37, A38, A44, A15;
A48: ts2 = tss by A13, TREES_4:15;
A49: for y being Nat st y in dom w3 holds
[(tsb . y),(tsa . y)] in R1 . (w3 /. y)

proof

let y be Nat; :: thesis:
assume A50: y in dom w3 ; :: thesis:
A51: tsb . y in rng ts by A48, A46, A50, FUNCT_1:3;
then reconsider t = tsb . y as Element of TS (DTConOSA X) by A9;
[t,(tsa . y)] in R2 . (w3 /. y) by A47, A50;
hence [(tsb . y),(tsa . y)] in R1 . (w3 /. y) by A8, A51; :: thesis:

end;

A52: the_result_sort_of o1 <= s by A5, A37, A38, A43, A44, A14, A15;
A53: the_result_sort_of o <= s by A5, A37, A38, A43, A44, A14, A15;
o ~= o1 by A5, A37, A38, A43, A44, A14, A15;
hence [(nt -tree ts),x] in R1 . s by A3, A38, A44, A15, A45, A53, A52, A46, A49; :: thesis:

end;

A54: for s being Symbol of (DTConOSA X) st s in Terminals (DTConOSA X) holds
S₃[ root-tree s]

proof

let sy be Symbol of (DTConOSA X); :: thesis:
assume sy in Terminals (DTConOSA X) ; :: thesis:
then consider s being Element of S, x being set such that
A55: x in X . s and
A56: sy = [x,s] by Th4;
let y be object ; :: thesis:
let s1 be Element of S; :: thesis:

hereby :: thesis:

assume A57: [(root-tree sy),y] in R1 . s1 ; :: thesis:
then A58: y = root-tree [x,s] by A2, A55, A56;
s <= s1 by A2, A55, A56, A57;
hence [(root-tree sy),y] in R2 . s1 by A4, A55, A56, A58; :: thesis:

end;

assume A59: [(root-tree sy),y] in R2 . s1 ; :: thesis:
then A60: y = root-tree [x,s] by A4, A55, A56;
s <= s1 by A4, A55, A56, A59;
hence [(root-tree sy),y] in R1 . s1 by A2, A55, A56, A60; :: thesis:

end;

A61: for t being DecoratedTree of the carrier of (DTConOSA X) st t in TS (DTConOSA X) holds
S₃[t] from DTCONSTR:sch 7(A54, A6);
for i being object st i in the carrier of S holds
R1 . i = R2 . i

proof

let i be object ; :: thesis:
assume i in the carrier of S ; :: thesis:
then reconsider s = i as Element of S ;
for a, b being object holds
( [a,b] in R1 . s iff [a,b] in R2 . s )

proof

let a, b be object ; :: thesis:
A62: the Sorts of (ParsedTermsOSA X) . s = ParsedTerms (X,s) by Def8
.= { a1 where a1 is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a1 . {} & the_result_sort_of o <= s ) ) } ;

hereby :: thesis:

assume A63: [a,b] in R1 . s ; :: thesis:
then a in the Sorts of (ParsedTermsOSA X) . s by ZFMISC_1:87;
then ex a1 being Element of TS (DTConOSA X) st
( a = a1 & ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a1 . {} & the_result_sort_of o <= s ) ) ) by A62;
hence [a,b] in R2 . s by A61, A63; :: thesis:

end;

assume A64: [a,b] in R2 . s ; :: thesis:
then a in the Sorts of (ParsedTermsOSA X) . s by ZFMISC_1:87;
then ex a1 being Element of TS (DTConOSA X) st
( a = a1 & ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a1 . {} & the_result_sort_of o <= s ) ) ) by A62;
hence [a,b] in R1 . s by A61, A64; :: thesis:

end;

hence R1 . i = R2 . i by RELAT_1:def 2; :: thesis:

end;

hence R1 = R2 ; :: thesis:

end;

A65: S₂[ PTCongruence X]

proof

let o1, o2 be OperSymbol of S; :: thesis:
let x1 be Element of Args (o1,(ParsedTermsOSA X)); :: thesis:
let x2 be Element of Args (o2,(ParsedTermsOSA X)); :: thesis:
let s3 be Element of S; :: thesis:
A66: dom (the_arity_of o2) = dom x2 by MSUALG_3:6;
A67: (PTCongruence X) . s3 = { [x3,y] where x3, y is Element of TS (DTConOSA X) : [x3,s3] in (PTClasses X) . y } by Def22;
reconsider ts2 = x2 as FinSequence of TS (DTConOSA X) by Th13;
A68: dom (the_arity_of o1) = dom x1 by MSUALG_3:6;
reconsider ts1 = x1 as FinSequence of TS (DTConOSA X) by Th13;
A69: rng ts1 c= TS (DTConOSA X) by FINSEQ_1:def 4;
reconsider x = (PTClasses X) * ts1 as FinSequence of bool [:(TS (DTConOSA X)), the carrier of S:] ;
dom (PTClasses X) = TS (DTConOSA X) by FUNCT_2:def 1;
then A70: len x = len ts1 by A69, FINSEQ_2:29;
then A71: dom x = dom ts1 by FINSEQ_3:29;
A72: OSSym (o1,X) ==> roots x1 by Th13;
then A73: (PTClasses X) . ((OSSym (o1,X)) -tree ts1) = @ ((OSSym (o1,X)),x) by Def21
.= { [((Den (o3,(ParsedTermsOSA X))) . x3),s4] where o3 is OperSymbol of S, x3 is Element of Args (o3,(ParsedTermsOSA X)), s4 is Element of S : ( ex o4 being OperSymbol of S st
( OSSym (o1,X) = [o4, the carrier of S] & o4 ~= o3 & len (the_arity_of o4) = len (the_arity_of o3) & the_result_sort_of o4 <= s4 & the_result_sort_of o3 <= s4 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x3 . y),(w3 /. y)] in x . y ) ) ) } ;
A74: OSSym (o2,X) ==> roots x2 by Th13;
then reconsider tx = (OSSym (o1,X)) -tree ts1, ty = (OSSym (o2,X)) -tree ts2 as Element of TS (DTConOSA X) by A72, Th12;
A75: (Den (o2,(ParsedTermsOSA X))) . x2 = ((PTOper X) . o2) . x2 by MSUALG_1:def 6
.= (PTDenOp (o2,X)) . ts2 by Def10
.= (OSSym (o2,X)) -tree ts2 by A74, Def9 ;
A76: (Den (o1,(ParsedTermsOSA X))) . x1 = ((PTOper X) . o1) . x1 by MSUALG_1:def 6
.= (PTDenOp (o1,X)) . ts1 by Def10
.= (OSSym (o1,X)) -tree ts1 by A72, Def9 ;
A77: rng ts2 c= TS (DTConOSA X) by FINSEQ_1:def 4;

hereby :: thesis:

assume [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in (PTCongruence X) . s3 ; :: thesis:
then consider t1, t2 being Element of TS (DTConOSA X) such that
A78: [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] = [t1,t2] and
A79: [t1,s3] in (PTClasses X) . t2 by A67;
A80: (Den (o1,(ParsedTermsOSA X))) . x1 = t1 by A78, XTUPLE_0:1;
A81: (Den (o2,(ParsedTermsOSA X))) . x2 = t2 by A78, XTUPLE_0:1;
[t2,s3] in (PTClasses X) . t1 by A79, Th19;
then consider o3 being OperSymbol of S, x3 being Element of Args (o3,(ParsedTermsOSA X)), s4 being Element of S such that
A82: [t2,s3] = [((Den (o3,(ParsedTermsOSA X))) . x3),s4] and
A83: ex o4 being OperSymbol of S st
( OSSym (o1,X) = [o4, the carrier of S] & o4 ~= o3 & len (the_arity_of o4) = len (the_arity_of o3) & the_result_sort_of o4 <= s4 & the_result_sort_of o3 <= s4 ) and
A84: ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x3 . y),(w3 /. y)] in x . y ) ) by A76, A73, A80;
consider o4 being OperSymbol of S such that
A85: OSSym (o1,X) = [o4, the carrier of S] and
A86: o4 ~= o3 and
A87: len (the_arity_of o4) = len (the_arity_of o3) and
A88: the_result_sort_of o4 <= s4 and
A89: the_result_sort_of o3 <= s4 by A83;
A90: o1 = o4 by A85, XTUPLE_0:1;
reconsider ts3 = x3 as FinSequence of TS (DTConOSA X) by Th13;
A91: OSSym (o3,X) ==> roots x3 by Th13;
A92: t2 = (Den (o3,(ParsedTermsOSA X))) . x3 by A82, XTUPLE_0:1;
A93: (Den (o3,(ParsedTermsOSA X))) . x3 = ((PTOper X) . o3) . x3 by MSUALG_1:def 6
.= (PTDenOp (o3,X)) . ts3 by Def10
.= (OSSym (o3,X)) -tree ts3 by A91, Def9 ;
then A94: OSSym (o3,X) = OSSym (o2,X) by A75, A81, A92, TREES_4:15;
s3 = s4 by A82, XTUPLE_0:1;
hence ( o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) by A86, A87, A88, A89, A90, A94, XTUPLE_0:1; :: thesis:
consider w3 being Element of the carrier of S * such that
A95: dom w3 = dom x and
A96: for y being Nat st y in dom x holds
[(x3 . y),(w3 /. y)] in x . y by A84;
take w3 = w3; :: thesis:
thus dom w3 = dom x1 by A70, A95, FINSEQ_3:29; :: thesis:
let y be Nat; :: thesis:
assume A97: y in dom w3 ; :: thesis:
A98: ts1 . y in rng ts1 by A71, A95, A97, FUNCT_1:3;
A99: ts3 = ts2 by A75, A81, A92, A93, TREES_4:15;
o3 = o2 by A94, XTUPLE_0:1;
then dom (the_arity_of o1) = dom (the_arity_of o2) by A87, A90, FINSEQ_3:29;
then ts2 . y in rng ts2 by A71, A68, A66, A95, A97, FUNCT_1:3;
then reconsider t22 = ts2 . y, t11 = ts1 . y as Element of TS (DTConOSA X) by A69, A77, A98;
[(x3 . y),(w3 /. y)] in x . y by A95, A96, A97;
then [(ts2 . y),(w3 /. y)] in (PTClasses X) . (ts1 . y) by A99, A95, A97, FUNCT_1:12;
then A100: [t11,(w3 /. y)] in (PTClasses X) . t22 by Th19;
(PTCongruence X) . (w3 /. y) = { [x5,y5] where x5, y5 is Element of TS (DTConOSA X) : [x5,(w3 /. y)] in (PTClasses X) . y5 } by Def22;
hence [(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y) by A100; :: thesis:

end;

assume that
A101: o1 ~= o2 and
A102: len (the_arity_of o1) = len (the_arity_of o2) and
A103: the_result_sort_of o1 <= s3 and
A104: the_result_sort_of o2 <= s3 and
A105: ex w3 being Element of the carrier of S * st
( dom w3 = dom x1 & ( for y being Nat st y in dom w3 holds
[(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y) ) ) ; :: thesis:
consider w3 being Element of the carrier of S * such that
A106: dom w3 = dom x1 and
A107: for y being Nat st y in dom w3 holds
[(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y) by A105;
for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y

proof

let y be Nat; :: thesis:
assume A108: y in dom x ; :: thesis:
A109: (PTCongruence X) . (w3 /. y) = { [x5,y5] where x5, y5 is Element of TS (DTConOSA X) : [x5,(w3 /. y)] in (PTClasses X) . y5 } by Def22;
[(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y) by A71, A106, A107, A108;
then consider x5, y5 being Element of TS (DTConOSA X) such that
A110: [(x1 . y),(x2 . y)] = [x5,y5] and
A111: [x5,(w3 /. y)] in (PTClasses X) . y5 by A109;
A112: x1 . y = x5 by A110, XTUPLE_0:1;
A113: x2 . y = y5 by A110, XTUPLE_0:1;
[y5,(w3 /. y)] in (PTClasses X) . x5 by A111, Th19;
hence [(x2 . y),(w3 /. y)] in x . y by A108, A112, A113, FUNCT_1:12; :: thesis:

end;

then [((Den (o2,(ParsedTermsOSA X))) . x2),s3] in (PTClasses X) . ((OSSym (o1,X)) -tree ts1) by A71, A73, A101, A102, A103, A104, A106;
then [tx,s3] in (PTClasses X) . ty by A75, Th19;
hence [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in (PTCongruence X) . s3 by A67, A76, A75; :: thesis:

end;

S₁[ PTCongruence X]

proof

let s1, s2 be Element of S; :: thesis:
let x be object ; :: thesis:
assume A114: x in X . s1 ; :: thesis:
reconsider sy = [x,s1] as Terminal of (DTConOSA X) by A114, Th4;
A115: (PTCongruence X) . s2 = { [x1,y] where x1, y is Element of TS (DTConOSA X) : [x1,s2] in (PTClasses X) . y } by Def22;
A116: root-tree [x,s1] in the Sorts of (ParsedTermsOSA X) . s1 by A114, Th10;

hereby :: thesis:

assume A117: s1 <= s2 ; :: thesis:
[(root-tree sy),s1] in (PTClasses X) . (root-tree sy) by A116, Th19;
then [(root-tree sy),s2] in (PTClasses X) . (root-tree sy) by A116, A117, Th21;
hence [(root-tree [x,s1]),(root-tree [x,s1])] in (PTCongruence X) . s2 by A115; :: thesis:

end;

let y be object ; :: thesis:
assume A118: ( [(root-tree [x,s1]),y] in (PTCongruence X) . s2 or [y,(root-tree [x,s1])] in (PTCongruence X) . s2 ) ; :: thesis:
then A119: root-tree [x,s1] in the Sorts of (ParsedTermsOSA X) . s2 by ZFMISC_1:87;
field ((PTCongruence X) . s2) = the Sorts of (ParsedTermsOSA X) . s2 by ORDERS_1:12;
then A120: (PTCongruence X) . s2 is_symmetric_in the Sorts of (ParsedTermsOSA X) . s2 by RELAT_2:def 11;
A121: (PTClasses X) . (root-tree sy) = @ sy by Def21
.= { [(root-tree sy),s3] where s3 is Element of S : ex s4 being Element of S ex x being set st
( x in X . s4 & sy = [x,s4] & s4 <= s3 ) } ;
y in the Sorts of (ParsedTermsOSA X) . s2 by A118, ZFMISC_1:87;
then [y,(root-tree sy)] in (PTCongruence X) . s2 by A120, A118, A119, RELAT_2:def 3;
then consider y1, r1 being Element of TS (DTConOSA X) such that
A122: [y,(root-tree sy)] = [y1,r1] and
A123: [y1,s2] in (PTClasses X) . r1 by A115;
A124: y = y1 by A122, XTUPLE_0:1;
root-tree sy = r1 by A122, XTUPLE_0:1;
then consider s3 being Element of S such that
A125: [y1,s2] = [(root-tree sy),s3] and
A126: ex s4 being Element of S ex x being set st
( x in X . s4 & sy = [x,s4] & s4 <= s3 ) by A121, A123;
s2 = s3 by A125, XTUPLE_0:1;
hence ( s1 <= s2 & y = root-tree [x,s1] ) by A124, A125, A126, XTUPLE_0:1; :: thesis:

end;

hence ( R = PTCongruence X iff ( ( for s1, s2 being Element of S
for x being object st x in X . s1 holds
( ( s1 <= s2 implies [(root-tree [x,s1]),(root-tree [x,s1])] in R . s2 ) & ( for y being object st ( [(root-tree [x,s1]),y] in R . s2 or [y,(root-tree [x,s1])] in R . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] ) ) ) ) & ( for o1, o2 being OperSymbol of S
for x1 being Element of Args (o1,(ParsedTermsOSA X))
for x2 being Element of Args (o2,(ParsedTermsOSA X))
for s3 being Element of S holds
( [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in R . s3 iff ( o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 & ex w3 being Element of the carrier of S * st
( dom w3 = dom x1 & ( for y being Nat st y in dom w3 holds
[(x1 . y),(x2 . y)] in R . (w3 /. y) ) ) ) ) ) ) ) by A1, A65; :: thesis: