:: deftheorem Def22 defines quasi_total MARGREL1:def 22 :
for A being set
for IT being PartFunc of (A *),A holds
( IT is quasi_total iff for x, y being FinSequence of A st len x = len y & x in dom IT holds
y in dom IT );