:: deftheorem Def1 defines Mpr1 MSUALG_9:def 1 :
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,B holds
( b₆ = Mpr1 F iff for i being set st i in I holds
b₆ . i = pr1 (F . i) );