:: deftheorem Def4 defines "" MSUALG_3:def 4 :
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds
for b₅ being ManySortedFunction of B,A holds
( b₅ = F "" iff for i being set st i in I holds
b₅ . i = (F . i) " );