:: deftheorem Def7 defines FuncSeq-like FUNCT_7:def 8 :
for IT being FinSequence holds
( IT is FuncSeq-like iff ex p being FinSequence st
( len p = (len IT) + 1 & ( for i being Nat st i in dom IT holds
IT . i in Funcs ((p . i),(p . (i + 1))) ) ) );