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