theorem :: SCPISORT:14

for n, p0 being Nat holds card (insert-sort (n,p0)) = 23