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