let x be set ; :: thesis: for T being Tree st x in T holds
x is FinSequence of NAT
let T be Tree; :: thesis: ( x in T implies x is FinSequence of NAT )
T c= NAT * by Def3;
hence ( x in T implies x is FinSequence of NAT ) by FINSEQ_1:def 11; :: thesis: verum