:: deftheorem Def2 defines Mpr2 MSUALG_9:def 2 :
for I being set
for A being ManySortedSet of I
for B, C being non-empty ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|]
for b₆ being ManySortedFunction of A,C holds
( b₆ = Mpr2 F iff for i being set st i in I holds
b₆ . i = pr2 (F . i) );