theorem :: MSAFREE5:9

for a being set
for w being DTree-yielding FinSequence holds dom (a -tree w) = {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } )