:: deftheorem Def10 defines id MSUALG_6:def 10 :
for I being set
for A being ManySortedSet of I
for b₃ being ManySortedRelation of A holds
( b₃ = id (I,A) iff for i being object st i in I holds
b₃ . i = id (A . i) );