let P be Instruction-Sequence of SCM+FSA; :: thesis: ( Bubble-Sort-Algorithm c= P implies for f being FinSeq-Location
for k being Nat st k < 53 holds
Bubble-Sort-Algorithm . k = P . k )
assume A1: Bubble-Sort-Algorithm c= P ; :: thesis: for f being FinSeq-Location
for k being Nat st k < 53 holds
Bubble-Sort-Algorithm . k = P . k
let f be FinSeq-Location ; :: thesis: for k being Nat st k < 53 holds
Bubble-Sort-Algorithm . k = P . k
let k be Nat; :: thesis: ( k < 53 implies Bubble-Sort-Algorithm . k = P . k )
assume A2: k < 53 ; :: thesis: Bubble-Sort-Algorithm . k = P . k
card (bubble-sort (fsloc 0)) = 53 by Th23;
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