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