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