Yes, I know what you mean, but there is a relationship, it is just that some of that relationship is described outside of Isabelle, but nevertheless provably. Ultimately, math is like that, provably so.

You could do what you want by making that argument explicit formally and machine-checked, but then you have to do a lot more work, by translating all of the components of the informal proof into formal ones. This will not give you any more insight than what the book already describes. But of course you could take it as an example of something that should be easy once you grasp the informal proof, but is actually quite a lot of work.