let j, i be Element of NAT ; :: thesis: ( j < i implies (elementary_tree i) | <*j*> = elementary_tree 0 )
set p = i |-> (elementary_tree 0 );
set T = tree (i |-> (elementary_tree 0 ));
assume A1: j < i ; :: thesis: (elementary_tree i) | <*j*> = elementary_tree 0
then A2: ( 1 + j >= 1 & j + 1 <= i ) by NAT_1:11, NAT_1:13;
len (i |-> (elementary_tree 0 )) = i by FINSEQ_1:def 18;
then A4: ( elementary_tree i = tree (i |-> (elementary_tree 0 )) & (tree (i |-> (elementary_tree 0 ))) | <*j*> = (i |-> (elementary_tree 0 )) . (j + 1) ) by A1, TREES_3:52, TREES_3:57;
j + 1 in Seg i by A2;
hence (elementary_tree i) | <*j*> = elementary_tree 0 by A4, FUNCOP_1:13; :: thesis: verum