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

(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