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

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