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 ( j + 1 = 1 + j & 1 + j >= 1 & j + 1 <= i & len (i |-> (elementary_tree 0 )) = i ) by FINSEQ_1:def 18, NAT_1:11, NAT_1:13;
then ( elementary_tree i = tree (i |-> (elementary_tree 0 )) & (tree (i |-> (elementary_tree 0 ))) | <*j*> = (i |-> (elementary_tree 0 )) . (j + 1) & j + 1 in Seg i ) by A1, TREES_3:52, TREES_3:57;
hence (elementary_tree i) | <*j*> = elementary_tree 0 by FUNCOP_1:13; :: thesis: verum