let f be FinSeq-Location ; :: thesis: for k being Nat st k < 71 holds
k in dom (insert-sort f)
let k be Nat; :: thesis: ( k < 71 implies k in dom (insert-sort f) )
assume A1: k < 71 ; :: thesis: k in dom (insert-sort f)
card (insert-sort f) = 71 by Th22;
hence k in dom (insert-sort f) by A1, AFINSQ_1:66; :: thesis: verum