set PTA = ParsedTermsOSA X;
set D = DTConOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
defpred S₁[ set , set , set ] means for R being monotone OSCongruence of ParsedTermsOSA X holds [$1,$2] in R . $3;
deffunc H₁( object ) -> set = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . $1 & y in the Sorts of (ParsedTermsOSA X) . $1 & ( for R being monotone OSCongruence of ParsedTermsOSA X holds [x,y] in R . $1 ) ) } ;
consider f being ManySortedSet of the carrier of S such that
A1: for i being object st i in the carrier of S holds
f . i = H₁(i) from PBOOLE:sch 4();
A2: for i being set st i in the carrier of S holds
f . i is Equivalence_Relation of ( the Sorts of (ParsedTermsOSA X) . i)

proof

let i be set ; :: thesis:
assume A3: i in the carrier of S ; :: thesis:
reconsider s = i as Element of S by A3;
A4: f . i = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . i & y in the Sorts of (ParsedTermsOSA X) . i & ( for R being monotone OSCongruence of ParsedTermsOSA X holds [x,y] in R . i ) ) } by A1, A3;

now :: thesis:

let z be object ; :: thesis:
assume z in f . i ; :: thesis:
then ex x, y being Element of TS (DTConOSA X) st
( z = [x,y] & x in the Sorts of (ParsedTermsOSA X) . i & y in the Sorts of (ParsedTermsOSA X) . i & S₁[x,y,i] ) by A4;
hence z in [:( the Sorts of (ParsedTermsOSA X) . i),( the Sorts of (ParsedTermsOSA X) . i):] by ZFMISC_1:87; :: thesis:

end;

then reconsider fi = f . i as Relation of ( the Sorts of (ParsedTermsOSA X) . i) by TARSKI:def 3;

now :: thesis:

let x, y, z be object ; :: thesis:
assume that
A5: x in the Sorts of (ParsedTermsOSA X) . s and
A6: y in the Sorts of (ParsedTermsOSA X) . s and
A7: z in the Sorts of (ParsedTermsOSA X) . s and
A8: [x,y] in fi and
A9: [y,z] in fi ; :: thesis:
thus [x,z] in fi :: thesis:

proof

reconsider t1 = x, t2 = y, t3 = z as Element of TS (DTConOSA X) by A5, A6, A7, Th15;
A10: ex t6, t7 being Element of TS (DTConOSA X) st
( [t2,t3] = [t6,t7] & t6 in the Sorts of (ParsedTermsOSA X) . i & t7 in the Sorts of (ParsedTermsOSA X) . i & S₁[t6,t7,i] ) by A4, A9;
A11: ex t4, t5 being Element of TS (DTConOSA X) st
( [t1,t2] = [t4,t5] & t4 in the Sorts of (ParsedTermsOSA X) . i & t5 in the Sorts of (ParsedTermsOSA X) . i & S₁[t4,t5,i] ) by A4, A8;

now :: thesis:

let R be monotone OSCongruence of ParsedTermsOSA X; :: thesis:
A12: [t2,t3] in R . s by A10;
field (R . s) = the Sorts of (ParsedTermsOSA X) . s by ORDERS_1:12;
then A13: R . s is_transitive_in the Sorts of (ParsedTermsOSA X) . s by RELAT_2:def 16;
[t1,t2] in R . s by A11;
hence [t1,t3] in R . s by A5, A6, A7, A12, A13, RELAT_2:def 8; :: thesis:

end;

hence [x,z] in fi by A4, A5, A7; :: thesis:

end;

then A14: fi is_transitive_in the Sorts of (ParsedTermsOSA X) . s by RELAT_2:def 8;

now :: thesis:

let x, y be object ; :: thesis:
assume that
A15: x in the Sorts of (ParsedTermsOSA X) . s and
A16: y in the Sorts of (ParsedTermsOSA X) . s and
A17: [x,y] in fi ; :: thesis:
thus [y,x] in fi :: thesis:

proof

reconsider t1 = x, t2 = y as Element of TS (DTConOSA X) by A15, A16, Th15;
A18: ex t3, t4 being Element of TS (DTConOSA X) st
( [t1,t2] = [t3,t4] & t3 in the Sorts of (ParsedTermsOSA X) . i & t4 in the Sorts of (ParsedTermsOSA X) . i & S₁[t3,t4,i] ) by A4, A17;

now :: thesis:

let R be monotone OSCongruence of ParsedTermsOSA X; :: thesis:
field (R . s) = the Sorts of (ParsedTermsOSA X) . s by ORDERS_1:12;
then A19: R . s is_symmetric_in the Sorts of (ParsedTermsOSA X) . s by RELAT_2:def 11;
[t1,t2] in R . s by A18;
hence [t2,t1] in R . s by A15, A16, A19, RELAT_2:def 3; :: thesis:

end;

hence [y,x] in fi by A4, A15, A16; :: thesis:

end;

then A20: fi is_symmetric_in the Sorts of (ParsedTermsOSA X) . s by RELAT_2:def 3;

now :: thesis:

let x be object ; :: thesis:
assume A21: x in the Sorts of (ParsedTermsOSA X) . s ; :: thesis:
thus [x,x] in fi :: thesis:

proof

reconsider t1 = x as Element of TS (DTConOSA X) by A21, Th15;

now :: thesis:

let R be monotone OSCongruence of ParsedTermsOSA X; :: thesis:
field (R . s) = the Sorts of (ParsedTermsOSA X) . s by ORDERS_1:12;
then R . s is_reflexive_in the Sorts of (ParsedTermsOSA X) . s by RELAT_2:def 9;
hence [t1,t1] in R . s by A21, RELAT_2:def 1; :: thesis:

end;

hence [x,x] in fi by A4, A21; :: thesis:

end;

then A22: fi is_reflexive_in the Sorts of (ParsedTermsOSA X) . s by RELAT_2:def 1;
then A23: field fi = the Sorts of (ParsedTermsOSA X) . s by ORDERS_1:13;
dom fi = the Sorts of (ParsedTermsOSA X) . s by A22, ORDERS_1:13;
hence f . i is Equivalence_Relation of ( the Sorts of (ParsedTermsOSA X) . i) by A23, A20, A14, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; :: thesis:

end;

then for i being set st i in the carrier of S holds
f . i is Relation of ( the Sorts of (ParsedTermsOSA X) . i),( the Sorts of (ParsedTermsOSA X) . i) ;
then reconsider f = f as ManySortedRelation of the Sorts of (ParsedTermsOSA X) by MSUALG_4:def 1;
reconsider f = f as ManySortedRelation of (ParsedTermsOSA X) ;
for i being set
for R being Relation of ( the Sorts of (ParsedTermsOSA X) . i) st i in the carrier of S & f . i = R holds
R is Equivalence_Relation of ( the Sorts of (ParsedTermsOSA X) . i) by A2;
then f is MSEquivalence_Relation-like by MSUALG_4:def 2;
then reconsider f = f as MSEquivalence-like ManySortedRelation of (ParsedTermsOSA X) by MSUALG_4:def 3;
f is os-compatible

proof

let s1, s2 be Element of S; :: according to OSALG_4:def 1 :: thesis:
assume A24: s1 <= s2 ; :: thesis:
A25: f . s1 = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 & S₁[x,y,s1] ) } by A1;
A26: f . s2 = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . s2 & y in the Sorts of (ParsedTermsOSA X) . s2 & S₁[x,y,s2] ) } by A1;
let x, y be set ; :: thesis:
assume that
A27: x in the Sorts of (ParsedTermsOSA X) . s1 and
A28: y in the Sorts of (ParsedTermsOSA X) . s1 ; :: thesis:

hereby :: thesis:

assume [x,y] in f . s1 ; :: thesis:
then consider t1, t2 being Element of TS (DTConOSA X) such that
A29: [x,y] = [t1,t2] and
A30: t1 in the Sorts of (ParsedTermsOSA X) . s1 and
A31: t2 in the Sorts of (ParsedTermsOSA X) . s1 and
A32: S₁[t1,t2,s1] by A25;

now :: thesis:

let R be monotone OSCongruence of ParsedTermsOSA X; :: thesis:
A33: R is os-compatible by OSALG_4:def 2;
[t1,t2] in R . s1 by A32;
then [t1,t2] in R . s2 by A24, A30, A31, A33;
hence ( t1 in the Sorts of (ParsedTermsOSA X) . s2 & t2 in the Sorts of (ParsedTermsOSA X) . s2 & [t1,t2] in R . s2 ) by ZFMISC_1:87; :: thesis:

end;

hence [x,y] in f . s2 by A26, A29; :: thesis:

end;

assume [x,y] in f . s2 ; :: thesis:
then consider t1, t2 being Element of TS (DTConOSA X) such that
A34: [x,y] = [t1,t2] and
t1 in the Sorts of (ParsedTermsOSA X) . s2 and
t2 in the Sorts of (ParsedTermsOSA X) . s2 and
A35: S₁[t1,t2,s2] by A26;
A36: y = t2 by A34, XTUPLE_0:1;

A37: now :: thesis:

let R be monotone OSCongruence of ParsedTermsOSA X; :: thesis:
A38: R is os-compatible by OSALG_4:def 2;
[t1,t2] in R . s2 by A35;
hence [t1,t2] in R . s1 by A24, A27, A28, A34, A38; :: thesis:

end;

x = t1 by A34, XTUPLE_0:1;
hence [x,y] in f . s1 by A25, A27, A28, A36, A37; :: thesis:

end;

then reconsider f = f as MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X by OSALG_4:def 2;
f is monotone

proof

let o1, o2 be OperSymbol of S; :: according to OSALG_4:def 26 :: thesis:
assume A39: o1 <= o2 ; :: thesis:
set w2 = the_arity_of o2;
set rs2 = the_result_sort_of o2;
let x1 be Element of Args (o1,(ParsedTermsOSA X)); :: thesis:
let x2 be Element of Args (o2,(ParsedTermsOSA X)); :: thesis:
assume A40: for y being Nat st y in dom x1 holds
[(x1 . y),(x2 . y)] in f . ((the_arity_of o2) /. y) ; :: thesis:
set D1 = (Den (o1,(ParsedTermsOSA X))) . x1;
set D2 = (Den (o2,(ParsedTermsOSA X))) . x2;

A41: now :: thesis:

let R be monotone OSCongruence of ParsedTermsOSA X; :: thesis:

A42: now :: thesis:

let y be Nat; :: thesis:
assume y in dom x1 ; :: thesis:
then A43: [(x1 . y),(x2 . y)] in f . ((the_arity_of o2) /. y) by A40;
f . ((the_arity_of o2) /. y) = { [x,z] where x, z is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o2) /. y) & z in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o2) /. y) & S₁[x,z,(the_arity_of o2) /. y] ) } by A1;
then ex x, z being Element of TS (DTConOSA X) st
( [(x1 . y),(x2 . y)] = [x,z] & x in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o2) /. y) & z in the Sorts of (ParsedTermsOSA X) . ((the_arity_of o2) /. y) & S₁[x,z,(the_arity_of o2) /. y] ) by A43;
hence [(x1 . y),(x2 . y)] in R . ((the_arity_of o2) /. y) ; :: thesis:

end;

end;

f . (the_result_sort_of o2) = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o2) & y in the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o2) & S₁[x,y, the_result_sort_of o2] ) } by A1;
hence [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in f . (the_result_sort_of o2) by A41; :: thesis:

end;

then reconsider f = f as MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X ;
take f ; :: thesis:
let R be monotone OSCongruence of ParsedTermsOSA X; :: thesis:
let i be object ; :: according to PBOOLE:def 2 :: thesis:
assume i in the carrier of S ; :: thesis:
then reconsider s = i as Element of S ;
A46: f . s = { [x,y] where x, y is Element of TS (DTConOSA X) : ( x in the Sorts of (ParsedTermsOSA X) . s & y in the Sorts of (ParsedTermsOSA X) . s & S₁[x,y,s] ) } by A1;
let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in f . i ; :: thesis:
then ex x, y being Element of TS (DTConOSA X) st
( z = [x,y] & x in the Sorts of (ParsedTermsOSA X) . s & y in the Sorts of (ParsedTermsOSA X) . s & S₁[x,y,s] ) by A46;
hence z in R . i ; :: thesis: