let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( Bubble-Sort-Algorithm c= P implies for f being FinSeq-Location
for k being Element of NAT st k < 63 holds
Bubble-Sort-Algorithm . k = P . k )
assume Z: Bubble-Sort-Algorithm c= P ; :: thesis: for f being FinSeq-Location
for k being Element of NAT st k < 63 holds
Bubble-Sort-Algorithm . k = P . k
let f be FinSeq-Location ; :: thesis: for k being Element of NAT st k < 63 holds
Bubble-Sort-Algorithm . k = P . k
let k be Element of NAT ; :: thesis: ( k < 63 implies Bubble-Sort-Algorithm . k = P . k )
assume A1: k < 63 ; :: thesis: Bubble-Sort-Algorithm . k = P . k
card (bubble-sort (fsloc 0)) = 63 by Th62;
then k in dom Bubble-Sort-Algorithm by A1, AFINSQ_1:70;
hence Bubble-Sort-Algorithm . k = P . k by Z, GRFUNC_1:8; :: thesis: verum