defpred S₁[ Element of 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 Function of NAT,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 & proj1 f = NAT & proj2 f = TrivialInfiniteTree )
thus f is one-to-one :: thesis: ( proj1 f = NAT & proj2 f = TrivialInfiniteTree )

proof

let x, y be set ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 f or not y in proj1 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: proj2 f = TrivialInfiniteTree
thus rng f c= TrivialInfiniteTree by RELAT_1:def 19; :: according to XBOOLE_0:def 10 :: thesis: TrivialInfiniteTree is_a_prefix_of proj2 f
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in TrivialInfiniteTree or a in proj2 f )
assume a in TrivialInfiniteTree ; :: thesis: a in proj2 f
then consider k being Element of NAT such that
A6: a = k |-> 0 ;
f . k = a by A2, A6;
hence a in proj2 f by A5, FUNCT_1:def 3; :: thesis: verum