defpred S₁[ Nat, set ] means $2 = $1 |-> 0;
A1: for x being Element of NAT ex y being Element of TrivialInfiniteTree st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of TrivialInfiniteTree st S₁[x,y]
x |-> 0 in TrivialInfiniteTree ;
then reconsider y = x |-> 0 as Element of TrivialInfiniteTree ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being sequence of TrivialInfiniteTree such that
A2: for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = NAT & rng f = TrivialInfiniteTree )
thus f is one-to-one :: thesis: ( dom f = NAT & rng f = TrivialInfiniteTree )

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume A3: ( x in dom f & y in dom f ) ; :: thesis: ( not f . x = f . y or x = y )
assume A4: f . x = f . y ; :: thesis: x = y
reconsider x = x, y = y as Element of NAT by A3, FUNCT_2:def 1;
( S₁[x,f . x] & S₁[y,f . y] ) by A2;
hence x = y by A4, FINSEQ_2:143; :: thesis: verum

end;

thus A5: dom f = NAT by FUNCT_2:def 1; :: thesis: rng f = TrivialInfiniteTree
thus rng f c= TrivialInfiniteTree by RELAT_1:def 19; :: according to XBOOLE_0:def 10 :: thesis: TrivialInfiniteTree is_a_prefix_of rng f
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in TrivialInfiniteTree or a in rng f )
assume a in TrivialInfiniteTree ; :: thesis: a in rng f
then consider k being Nat such that
A6: a = k |-> 0 ;
A7: k in NAT by ORDINAL1:def 12;
then f . k = a by A2, A6;
hence a in rng f by A5, FUNCT_1:def 3, A7; :: thesis: verum