The source follows the book: the state transformations of the prefixes of the input are computed by a composition of primes (Lemma A.2.5, $Transducers.stateTransTransducer_prime_decomposition$, an induction on the number of states and on the number of letters whose state transformation is not a permutation, the letter $a$ of the induction step being made to act as the identity rather than removed from the alphabet), they are paired with the input letters, and the output is produced by a flip-flop delay machine. The bridge transports the family of primes and the composition closure ($compClosure_iff$).

Theorem A.2.2 of Transducers (the Krohn–Rhodes theorem, in the form the book proves); Lean proof by Aristotle ($Transducers.krohn_rhodes$, $RequestProject/PartA/StateTrans.lean$).