:: deftheorem Def1 defines || MSAFREE:def 1 :
for I being set
for A, B being ManySortedSet of I
for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for b₆ being ManySortedFunction of C,B holds
( b₆ = F || C iff for i being set st i in I holds
b₆ . i = (F . i) | (C . i) );