:: deftheorem defines Func_Seq BHSP_5:def 4 :
for DK, DX being non empty set
for F being Function of DX,DK
for p being FinSequence of DX holds Func_Seq (F,p) = F * p;