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 A2: ( len x = len y & x in dom f ) ; :: thesis: y in dom f
thus y in dom f by A1, A2, UNIALG_1:def 2; :: thesis: verum