defpred S₁[ 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 S₁[x,y] ) ) & ( for x, y being SortSymbol of S holds
( [x,y] in R2 iff S₁[x,y] ) ) holds
R1 = R2 from PUA2MSS1:sch 2();
hence for b₁, b₂ being Relation of the carrier of S st ( for s1, s2 being SortSymbol of S holds
( [s1,s2] in b₁ 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 b₂ 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
b₁ = b₂ ; :: thesis: verum