ext
V : Type u_1
inst✝ : Zermelo V
r x y z t s : V
⊢ rcomp (rcomp t s) r = rcomp t (rcomp s r)
case h
V : Type u_1
inst✝ : Zermelo V
r x y z t s z✝ : V
⊢ z✝ ∈ rcomp (rcomp t s) r ↔ z✝ ∈ rcomp t (rcomp s r)