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 5 :: thesis: ( ( for b₁ being FinSequence of NAT holds
( not b₁ in TrivialInfiniteTree or ProperPrefixes b₁ c= TrivialInfiniteTree ) ) & ( for b₁ being FinSequence of NAT
for b₂, b₃ being Element of NAT holds
( not b₁ ^ <*b₂*> in TrivialInfiniteTree or not b₃ <= b₂ or b₁ ^ <*b₃*> 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 ;
then x is FinSequence of NAT by FINSEQ_2:77;
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 b₁ being FinSequence of NAT
for b₂, b₃ being Element of NAT holds
( not b₁ ^ <*b₂*> in TrivialInfiniteTree or not b₃ <= b₂ or b₁ ^ <*b₃*> 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 TREES_1:35;
A3: len x = len ((len x) |-> 0 ) by FINSEQ_1:def 18;
for k being Nat st 1 <= k & k <= len x holds
x . k = ((len x) |-> 0 ) . k

proof

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 A4: k in dom x by FINSEQ_3:27;
then A5: k in Seg (len x) by FINSEQ_1:def 3;
len x < len p by A2, TREES_1:37;
then Seg (len x) c= Seg (len p) by FINSEQ_1:7;
then k in Seg (len p) by A5;
then A6: k in Seg m by A1, FINSEQ_1:def 18;
x is_a_proper_prefix_of p by A2, TREES_1:36;
then A7: x c= p by XBOOLE_0:def 8;
thus ((len x) |-> 0 ) . k = 0 by A5, FUNCOP_1:13
.= p . k by A1, A6, FUNCOP_1:13
.= x . k by A4, A7, GRFUNC_1:8 ; :: thesis: verum

end;

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

end;

let p be FinSequence of NAT ; :: thesis: for b₁, b₂ being Element of NAT holds
( not p ^ <*b₁*> in TrivialInfiniteTree or not b₂ <= b₁ or p ^ <*b₂*> in TrivialInfiniteTree )
let m, n be Element of NAT ; :: thesis: ( not p ^ <*m*> in TrivialInfiniteTree or not n <= m or 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 ;
assume A9: n <= m ; :: thesis: p ^ <*n*> in TrivialInfiniteTree
A10: len (p ^ <*m*>) = (len p) + 1 by FINSEQ_2:19;
A11: len (p ^ <*m*>) = k by A8, FINSEQ_1:def 18;
A12: (p ^ <*m*>) . (len (p ^ <*m*>)) = m by A10, FINSEQ_1:59;
( 0 = k or 0 < k ) ;
then 0 + 1 <= k by A8, NAT_1:13;
then k in Seg k by FINSEQ_1:3;
then A13: m = 0 by A8, A11, A12, FUNCOP_1:13;
A14: len (p ^ <*n*>) = len ((len (p ^ <*n*>)) |-> 0 ) by FINSEQ_1:def 18;
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 that
A15: 1 <= z and
A16: z <= len (p ^ <*n*>) ; :: thesis: ((len (p ^ <*n*>)) |-> 0 ) . z = (p ^ <*n*>) . z
z in dom (p ^ <*n*>) by A15, A16, FINSEQ_3:27;
then A17: z in Seg (len (p ^ <*n*>)) by FINSEQ_1:def 3;
len (p ^ <*n*>) = (len p) + 1 by FINSEQ_2:19;
then A18: z in Seg k by A10, A11, A15, A16, FINSEQ_1:3;
thus ((len (p ^ <*n*>)) |-> 0 ) . z = 0 by A17, FUNCOP_1:13
.= (p ^ <*m*>) . z by A8, A18, FUNCOP_1:13
.= (p ^ <*n*>) . z by A9, A13 ; :: thesis: verum

end;

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