:: deftheorem Def12 defines supp_restr GROUP_21:def 12 :
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for x being Function
for b₅ being disjoint_valued ManySortedSet of I holds
( b₅ = supp_restr (x,F) iff for i being Element of I holds b₅ . i = support ((x | (J . i)),(F . i)) );