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