let P be Instruction-Sequence of SCM+FSA; :: 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 A1: 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 A2: 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 A2, AFINSQ_1:66;
hence Bubble-Sort-Algorithm . k = P . k by A1, GRFUNC_1:2; :: thesis: verum