let f be PartFunc of (NAT * ),NAT ; :: thesis: ( f is quasi_total implies f is len-total )
assume A1: f is quasi_total ; :: thesis: f is len-total
let x, y be FinSequence of NAT ; :: according to COMPUT_1:def 3 :: thesis: ( len x = len y & x in dom f implies y in dom f )
assume that
A2: len x = len y and
A3: x in dom f ; :: thesis: y in dom f
thus y in dom f by A1, A2, A3, MARGREL1:def 23; :: thesis: verum