∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply X Y) (difference X (difference X Y)).
∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (difference (difference X Y) Z) (difference (difference X Z) (difference Y Z)).
∀H2:∀X:Univ.∀Y:Univ.eq Univ (difference X (difference X Y)) (difference Y (difference Y X)).
∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply X Y) (difference X (difference X Y)).
∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (difference (difference X Y) Z) (difference (difference X Z) (difference Y Z)).
∀H2:∀X:Univ.∀Y:Univ.eq Univ (difference X (difference X Y)) (difference Y (difference Y X)).