defpred S₁[ set , set ] means ex o being OperSymbol of 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 , st
for x, y being SortSymbol of holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
hence ex b₁ being Relation of st
for s1, s2 being SortSymbol of holds
( [s1,s2] in b₁ iff ex o being OperSymbol of 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