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 2 :: 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 22; :: thesis: verum