let n be Element of NAT ; :: thesis: TrivialInfiniteTree -level n = {(n |-> 0 )}
set T = TrivialInfiniteTree ;
set L = { w where w is Element of TrivialInfiniteTree : len w = n } ;
set f = n |-> 0 ;
{(n |-> 0 )} = { w where w is Element of TrivialInfiniteTree : len w = n }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { w where w is Element of TrivialInfiniteTree : len w = n } c= {(n |-> 0 )}

let a be set ; :: thesis: ( a in {(n |-> 0 )} implies a in { w where w is Element of TrivialInfiniteTree : len w = n } )
assume a in {(n |-> 0 )} ; :: thesis: a in { w where w is Element of TrivialInfiniteTree : len w = n }
then A1: a = n |-> 0 by TARSKI:def 1;
A2: n |-> 0 in TrivialInfiniteTree ;
len (n |-> 0 ) = n by FINSEQ_1:def 18;
hence a in { w where w is Element of TrivialInfiniteTree : len w = n } by A1, A2; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { w where w is Element of TrivialInfiniteTree : len w = n } or a in {(n |-> 0 )} )
assume a in { w where w is Element of TrivialInfiniteTree : len w = n } ; :: thesis: a in {(n |-> 0 )}
then consider w being Element of TrivialInfiniteTree such that
A3: ( a = w & len w = n ) ;
w in TrivialInfiniteTree ;
then ex k being Element of NAT st w = k |-> 0 ;
then a = n |-> 0 by A3, FINSEQ_1:def 18;
hence a in {(n |-> 0 )} by TARSKI:def 1; :: thesis: verum

end;

hence TrivialInfiniteTree -level n = {(n |-> 0 )} by TREES_2:def 6; :: thesis: verum