:: deftheorem defines .. FINSEQ_4:def 4 :
for p being FinSequence
for x being object holds x .. p = (Sgm (p " {x})) . 1;