let i be Nat; :: thesis: for j being Element of NAT st j < i holds
(elementary_tree i) | <*j*> = elementary_tree 0
let j 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 CARD_1:def 7;
then A3: ( elementary_tree i = tree (i |-> (elementary_tree 0)) & (tree (i |-> (elementary_tree 0))) | <*j*> = (i |-> (elementary_tree 0)) . (j + 1) ) by A1, TREES_3:49, TREES_3:54;
j + 1 in Seg i by A2;
hence (elementary_tree i) | <*j*> = elementary_tree 0 by A3, FUNCOP_1:7; :: thesis: verum