let i be Nat; :: thesis: elementary_tree i = tree (i |-> (elementary_tree 0))
set p = i |-> (elementary_tree 0);
let q be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not q in elementary_tree i or q in tree (i |-> (elementary_tree 0)) ) & ( not q in tree (i |-> (elementary_tree 0)) or q in elementary_tree i ) )
A1: len (i |-> (elementary_tree 0)) = i by CARD_1:def 7;
then elementary_tree i c= tree (i |-> (elementary_tree 0)) by Th53;
hence ( q in elementary_tree i implies q in tree (i |-> (elementary_tree 0)) ) ; :: thesis: ( not q in tree (i |-> (elementary_tree 0)) or q in elementary_tree i )
assume q in tree (i |-> (elementary_tree 0)) ; :: thesis: q in elementary_tree i
then A2: ( q = {} or ex n being Nat ex r being FinSequence st
( n < len (i |-> (elementary_tree 0)) & r in (i |-> (elementary_tree 0)) . (n + 1) & q = <*n*> ^ r ) ) by Def15;

now :: thesis: ( ex n being Nat ex r being FinSequence st
( n < len (i |-> (elementary_tree 0)) & r in (i |-> (elementary_tree 0)) . (n + 1) & q = <*n*> ^ r ) implies q in elementary_tree i )

given n being Nat, r being FinSequence such that A3: n < len (i |-> (elementary_tree 0)) and
A4: r in (i |-> (elementary_tree 0)) . (n + 1) and
A5: q = <*n*> ^ r ; :: thesis: q in elementary_tree i
i |-> (elementary_tree 0) = (Seg i) --> (elementary_tree 0) by FINSEQ_2:def 2;
then A6: rng (i |-> (elementary_tree 0)) c= {(elementary_tree 0)} by FUNCOP_1:13;
(i |-> (elementary_tree 0)) . (n + 1) in rng (i |-> (elementary_tree 0)) by A3, Lm3;
then (i |-> (elementary_tree 0)) . (n + 1) = elementary_tree 0 by A6, TARSKI:def 1;
then r = {} by A4, TARSKI:def 1, TREES_1:29;
then q = <*n*> by A5, FINSEQ_1:34;
hence q in elementary_tree i by A1, A3, TREES_1:28; :: thesis: verum

end;

hence q in elementary_tree i by A2, TREES_1:22; :: thesis: verum