:: deftheorem Def9 defines FuncSequence FUNCT_7:def 10 :
for q being non empty non-empty FinSequence
for b₂ being FinSequence holds
( b₂ is FuncSequence of q iff ( (len b₂) + 1 = len q & ( for i being Nat st i in dom b₂ holds
b₂ . i in Funcs ((q . i),(q . (i + 1))) ) ) );