:: deftheorem Def3 defines compose FUNCT_7:def 4 :
for X being set
for p being Function-yielding FinSequence
for b₃ being Function holds
( b₃ = compose (p,X) iff ex f being ManySortedFunction of NAT st
( b₃ = f . (len p) & f . 0 = id X & ( for i being Nat st i + 1 in dom p holds
for g, h being Function st g = f . i & h = p . (i + 1) holds
f . (i + 1) = h * g ) ) );