let p be Tree-yielding FinSequence; :: thesis: for k being Element of NAT st k + 1 in dom p holds
(tree p) | <*k*> = p . (k + 1)
let k be Element of NAT ; :: thesis: ( k + 1 in dom p implies (tree p) | <*k*> = p . (k + 1) )
assume k + 1 in dom p ; :: thesis: (tree p) | <*k*> = p . (k + 1)
then k + 1 <= len p by FINSEQ_3:25;
then k < len p by NAT_1:13;
hence (tree p) | <*k*> = p . (k + 1) by TREES_3:49; :: thesis: verum