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