let f be FinSeq-Location ; :: thesis: for k being Element of NAT st k < 82 holds
k in dom (insert-sort f)
let k be Element of NAT ; :: thesis: ( k < 82 implies k in dom (insert-sort f) )
assume A1: k < 82 ; :: thesis: k in dom (insert-sort f)
card (insert-sort f) = 82 by Th42;
hence k in dom (insert-sort f) by A1, AFINSQ_1:70; :: thesis: verum