let k, k9 be Element of NAT ; :: thesis: ( x. k = v1 & x. k9 = v1 implies k = k9 )
assume ( x. k = v1 & x. k9 = v1 ) ; :: thesis: k = k9
then ( 5 + k = v1 & 5 + k9 = v1 ) by ZF_LANG:def 2;
hence k = k9 by XCMPLX_1:2; :: thesis: verum