∀H1:∀X:Univ.∀Y:Univ.eq Univ (multiply (inverse Y) Y X) X.
∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply X X Y) X.
∀H3:∀X:Univ.∀Y:Univ.eq Univ (multiply Y X X) X.
∀H1:∀X:Univ.∀Y:Univ.eq Univ (multiply (inverse Y) Y X) X.
∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply X X Y) X.
∀H3:∀X:Univ.∀Y:Univ.eq Univ (multiply Y X X) X.