:: deftheorem Def1 defines ManySortedRelation MSUALG_4:def 1 :
for I being set
for A, B, b₄ being ManySortedSet of I holds
( b₄ is ManySortedRelation of A,B iff for i being set st i in I holds
b₄ . i is Relation of (A . i),(B . i) );