:: deftheorem Def4 defines apply FUNCT_7:def 5 :
for p being Function-yielding FinSequence
for x being object
for b₃ being FinSequence holds
( b₃ = apply (p,x) iff ( len b₃ = (len p) + 1 & b₃ . 1 = x & ( for i being Nat
for f being Function st i in dom p & f = p . i holds
b₃ . (i + 1) = f . (b₃ . i) ) ) );