-∀H0:∀U:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply U (inverse (multiply Y (multiply (multiply (multiply Z (inverse Z)) (inverse (multiply U Y))) U)))) U.eq Univ (multiply x (inverse (multiply y (multiply (multiply (multiply z (inverse z)) (inverse (multiply u y))) x)))) u
+∀H0:∀U:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply U (inverse (multiply Y (multiply (multiply (multiply Z (inverse Z)) (inverse (multiply U Y))) U)))) U.eq Univ (multiply x (inverse (multiply y (multiply (multiply (multiply z (inverse z)) (inverse (multiply u y))) x)))) u)