Nincs időm végiggondolni a bizonyítást, de ha jól sejtem, azt kell csinálni (vagy úgy is lehet csinálni), hogy vesszük az első |K| elemű oszlop által generált ideált (ami főideál), annak egy generátorát stb. és így n lépésben sorra megkapjuk a keresett bázist és együtthatókat. Tehát igazából véges sok lépésben megy a dolog, felhasználva, hogy R-ben minden ideál főideál. Az euklideszi algoritmus valószínűleg csak ködösítés, pontosabban ez az algoritmus garantálni tudja, hogy minden ideál főideál legyen, de ennek bizonyításában sincs szükség végtelen sok lépésre.

Másfelől olyan nagyon is van és elterjedt a matematikában, hogy végtelen sok lépésben definiálunk valamit (pl. egy függvényt). Nevezheted eljárásnak, de valójában definícióról van szó (amihez esetleg fel kell használni egy kiválasztási függvényt, amiért a végtermék nem lesz kanonikus). Ezt transzfinit rekurziónak hívják, és a halmazelmélet egyik alapvető fogalma (http://www.encyclopediaofmath.org/index.php/Transfinite_recursion). Elképzelhető, hogy az említett bizonyítás (ahogy az órán elhangzott) ilyet használ vagy legalábbis ezzel lehetne formalizálni: tehát rekurzívan megy végig a mátrixelemeken és definiál hozzájuk rendelt mennyiségeket. De mint mondtam, szerintem erre nincs szükség, a |K|xn-es mátrix csak szemléletesebbé teszi a bizonyítást, aminek ötlete, hogy bizonyos együtthatóhalmazok legnagyobb közös osztóját tekinti (tehát az általuk generált ideál egy generátorelemét).