DanielFilan comments on Multiplicative Operations on Cartesian Frames

[DanielFilan]

And in my proof the morphism isn’t bijective.