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

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