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

(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