:: deftheorem defines - FINSEQ_3:def 1 :
for p being FinSequence
for A being set holds p - A = p * (Sgm ((dom p) \ (p " A)));