theorem ThL0: :: MSAFREE5:15

for p being non empty Tree-yielding FinSequence holds Leaves (tree p) = { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) }