:: deftheorem Def10 defines decomp NUMBER17:def 10 :
for D being non empty set
for A being b₁ -FinSequence-membered set
for b₃ being Relation holds
( b₃ = decomp A iff for x, y being object holds
( [x,y] in b₃ iff ( x in D & ex f being FinSequence of D st
( y = f & <*x*> ^ f in A ) ) ) );