theorem :: MSUALG_9:23

for I being set
for A, M being ManySortedSet of I
for B, C being non-empty ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st M in doms F holds
for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]