reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
let x be Element of NatEmbSeq . n; :: thesis: ( x is Function-like & x is Relation-like )
A1: x in NatEmbSeq . n9 ;
NatEmbSeq . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by Def5;
then ex f being Element of Funcs ((Seg n),(Seg (n + 1))) st
( x = f & @ f is increasing ) by A1;
hence ( x is Function-like & x is Relation-like ) ; :: thesis: verum