set X = TrivialInfiniteTree ;
0 |-> 0 in TrivialInfiniteTree ;
hence not TrivialInfiniteTree is empty ; :: thesis: TrivialInfiniteTree is Tree-like
thus TrivialInfiniteTree c= NAT * :: according to TREES_1:def 3 :: thesis: ( ( for p being FinSequence of NAT st p in TrivialInfiniteTree holds
ProperPrefixes p c= TrivialInfiniteTree ) & ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in TrivialInfiniteTree & n <= k holds
p ^ <*n*> in TrivialInfiniteTree ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in TrivialInfiniteTree or x in NAT * )
assume x in TrivialInfiniteTree ; :: thesis: x in NAT *
then ex k being Element of NAT st x = k |-> 0 ;
hence x in NAT * by FINSEQ_1:def 11; :: thesis: verum

end;

thus for p being FinSequence of NAT st p in TrivialInfiniteTree holds
ProperPrefixes p c= TrivialInfiniteTree :: thesis: for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in TrivialInfiniteTree & n <= k holds
p ^ <*n*> in TrivialInfiniteTree

proof

let p be FinSequence of NAT ; :: thesis: ( p in TrivialInfiniteTree implies ProperPrefixes p c= TrivialInfiniteTree )
assume p in TrivialInfiniteTree ; :: thesis: ProperPrefixes p c= TrivialInfiniteTree
then consider m being Element of NAT such that
A1: p = m |-> 0 ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes p or x in TrivialInfiniteTree )
assume A2: x in ProperPrefixes p ; :: thesis: x in TrivialInfiniteTree
then reconsider x = x as FinSequence by Th35;
A3: for k being Nat st 1 <= k & k <= len x holds
x . k = ((len x) |-> 0) . k

proof

x is_a_proper_prefix_of p by A2, Th36;
then A4: x c= p by XBOOLE_0:def 8;
let k be Nat; :: thesis: ( 1 <= k & k <= len x implies x . k = ((len x) |-> 0) . k )
assume ( 1 <= k & k <= len x ) ; :: thesis: x . k = ((len x) |-> 0) . k
then A5: k in dom x by FINSEQ_3:25;
then A6: k in Seg (len x) by FINSEQ_1:def 3;
len x < len p by A2, Th37;
then Seg (len x) c= Seg (len p) by FINSEQ_1:5;
then k in Seg (len p) by A6;
then A7: k in Seg m by A1, CARD_1:def 7;
thus ((len x) |-> 0) . k = 0 by A6, FUNCOP_1:7
.= p . k by A1, A7, FUNCOP_1:7
.= x . k by A5, A4, GRFUNC_1:2 ; :: thesis: verum

end;

len x = len ((len x) |-> 0) by CARD_1:def 7;
then x = (len x) |-> 0 by A3, FINSEQ_1:14;
hence x in TrivialInfiniteTree ; :: thesis: verum

end;

let p be FinSequence of NAT ; :: thesis: for k, n being Element of NAT st p ^ <*k*> in TrivialInfiniteTree & n <= k holds
p ^ <*n*> in TrivialInfiniteTree
let m, n be Element of NAT ; :: thesis: ( p ^ <*m*> in TrivialInfiniteTree & n <= m implies p ^ <*n*> in TrivialInfiniteTree )
assume p ^ <*m*> in TrivialInfiniteTree ; :: thesis: ( not n <= m or p ^ <*n*> in TrivialInfiniteTree )
then consider k being Element of NAT such that
A8: p ^ <*m*> = k |-> 0 ;
( 0 = k or 0 < k ) ;
then 0 + 1 <= k by A8, NAT_1:13;
then A9: k in Seg k by FINSEQ_1:1;
assume A10: n <= m ; :: thesis: p ^ <*n*> in TrivialInfiniteTree
A11: len (p ^ <*m*>) = k by A8, CARD_1:def 7;
A12: len (p ^ <*m*>) = (len p) + 1 by FINSEQ_2:16;
then (p ^ <*m*>) . (len (p ^ <*m*>)) = m by FINSEQ_1:42;
then A13: m = 0 by A8, A11, A9, FUNCOP_1:7;
A14: for z being Nat st 1 <= z & z <= len (p ^ <*n*>) holds
((len (p ^ <*n*>)) |-> 0) . z = (p ^ <*n*>) . z

proof

let z be Nat; :: thesis: ( 1 <= z & z <= len (p ^ <*n*>) implies ((len (p ^ <*n*>)) |-> 0) . z = (p ^ <*n*>) . z )
assume A15: ( 1 <= z & z <= len (p ^ <*n*>) ) ; :: thesis: ((len (p ^ <*n*>)) |-> 0) . z = (p ^ <*n*>) . z
len (p ^ <*n*>) = (len p) + 1 by FINSEQ_2:16;
then A16: z in Seg k by A12, A11, A15, FINSEQ_1:1;
z in dom (p ^ <*n*>) by A15, FINSEQ_3:25;
then z in Seg (len (p ^ <*n*>)) by FINSEQ_1:def 3;
hence ((len (p ^ <*n*>)) |-> 0) . z = 0 by FUNCOP_1:7
.= (p ^ <*m*>) . z by A8, A16, FUNCOP_1:7
.= (p ^ <*n*>) . z by A10, A13 ;
:: thesis: verum

end;

len (p ^ <*n*>) = len ((len (p ^ <*n*>)) |-> 0) by CARD_1:def 7;
then (len (p ^ <*n*>)) |-> 0 = p ^ <*n*> by A14, FINSEQ_1:14;
hence p ^ <*n*> in TrivialInfiniteTree ; :: thesis: verum