reconsider mk = mk as Element of NAT by ORDINAL1:def 12;
take mk ; :: thesis: ex mk being Element of NAT st
( <*mk*> = x `2_3 & mk = <*mk*> /. 1 )
take mk ; :: thesis: ( <*mk*> = x `2_3 & mk = <*mk*> /. 1 )
thus ( <*mk*> = x `2_3 & mk = <*mk*> /. 1 ) by A1, FINSEQ_4:16; :: thesis: verum