that's v neat @Sophie – one slight typo: the line \\(f(s) \otimes f(s') = f(s \otimes s')\\) should be \\(f(s) \otimes f(s') \cong f(s \otimes s')\\)