:: deftheorem Def9 defines App HILB10_7:def 9 :
for F being FinSequence-yielding FinSequence
for b₂ being FinSequence-yielding Function holds
( b₂ = App F iff ( dom b₂ = doms F & ( for p being FinSequence st p in doms F holds
( len (b₂ . p) = len p & ( for i being Nat st i in dom p holds
(b₂ . p) . i = (F . i) . (p . i) ) ) ) ) );