[2] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, <em>Intelligent Computer Mathematics</em>, volume 9150 of <em>Lecture Notes in Computer Science</em>, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:<a href="https://doi.org/10.1007/978-3-319-20615-817." target="_blank" rel="noopener noreferrer" class="text-signal-blue hover:underline">10.1007/978-3-319-20615-817.</a><pub-id pub-id-type="doi"><a href="https://doi.org/10.1007/978-3-319-20615-817" target="_blank" rel="noopener noreferrer" class="text-signal-blue hover:underline">10.1007/978-3-319-20615-817</a></pub-id>
[11] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. <em>Formalized Mathematics</em>, 1(<bold>3</bold>):569–573, 1990.
[12] E. B. Vinberg. <em>A Course in Algebra</em>. American Mathematical Society, 2003. ISBN 0821834134.<dgdoi:pub-id xmlns:dgdoi="http://degruyter.com/resources/doi-from-crossref" pub-id-type="doi"><a href="https://doi.org/10.1090/gsm/056" target="_blank" rel="noopener noreferrer" class="text-signal-blue hover:underline">10.1090/gsm/056</a></dgdoi:pub-id>