:: deftheorem Def2 defines len-total COMPUT_1:def 2 :
for f being NAT * -defined Relation holds
( f is len-total iff for x, y being FinSequence of NAT st len x = len y & x in dom f holds
y in dom f );