:: deftheorem defines quasi_total MARGREL1:def 24 :
for A being set
for IT being PFuncFinSequence of A holds
( IT is quasi_total iff for n being Nat
for h being PartFunc of (A *),A st n in dom IT & h = IT . n holds
h is quasi_total );