:: deftheorem Def1 defines id MSUALG_3:def 1 :
for I being set
for A being ManySortedSet of I
for b₃ being ManySortedFunction of A,A holds
( b₃ = id A iff for i being set st i in I holds
b₃ . i = id (A . i) );