reconsider s = {} as FinSequence of NAT by TREES_1:47;
let Z be Tree; :: thesis: for n, m being Element of NAT st n <= m & <*m*> in Z holds
<*n*> in Z
let n, m be Element of NAT ; :: thesis: ( n <= m & <*m*> in Z implies <*n*> in Z )
assume that
A1: n <= m and
A2: <*m*> in Z ; :: thesis: <*n*> in Z
{} ^ <*m*> in Z by A2, FINSEQ_1:47;
then s ^ <*n*> in Z by A1, TREES_1:def 5;
hence <*n*> in Z by FINSEQ_1:47; :: thesis: verum