:: deftheorem Def8 defines (\) SETLIM_2:def 8 :
for X being set
for A1 being SetSequence of X
for A being Subset of X
for b₄ being SetSequence of X holds
( b₄ = A1 (\) A iff for n being Nat holds b₄ . n = (A1 . n) \ A );